1    λ(f : Type → Type → Type)
 2  →   { first :
 3            ∀(a : Type)
 4          → ∀(b : Type)
 5          → ∀(c : Type)
 6          → f a b
 7          → f { _1 : a, _2 : c } { _1 : b, _2 : c }
 8      , second :
 9            ∀(a : Type)
10          → ∀(b : Type)
11          → ∀(c : Type)
12          → f b c
13          → f { _1 : a, _2 : b } { _1 : a, _2 : c }
14      }
15    ⩓ ./../Profunctor/Type f