1    λ(f : Type → Type → Type)
 2  →   { arr :
 3          ∀(a : Type) → ∀(b : Type) → (a → b) → f a b
 4      , split :
 5            ∀(a : Type)
 6          → ∀(b : Type)
 7          → ∀(c : Type)
 8          → ∀(d : Type)
 9          → f a b
10          → f c d
11          → f { _1 : a, _2 : c } { _1 : b, _2 : d }
12      , fanout :
13            ∀(a : Type)
14          → ∀(b : Type)
15          → ∀(c : Type)
16          → f a b
17          → f a c
18          → f a { _1 : b, _2 : c }
19      }
20    ⩓ ./../Category/Type f
21    ⩓ ./../Strong/Type f