1      { first =
 2            λ(a : Type)
 3          → λ(b : Type)
 4          → λ(c : Type)
 5          → λ(f : a → b)
 6          → λ(p : { _1 : a, _2 : c })
 7          → { _1 = f p._1, _2 = p._2 }
 8      , second =
 9            λ(a : Type)
10          → λ(b : Type)
11          → λ(c : Type)
12          → λ(f : b → c)
13          → λ(p : { _1 : a, _2 : b })
14          → { _1 = p._1, _2 = f p._2 }
15      }
16    ∧ ./profunctor
17  : ./../Strong/Type ./Type