1    λ(h : Type → Type)
 2  → λ(functor : ./../Functor/Type h)
 3  → λ(f : Type → Type)
 4  → λ(g : Type → Type)
 5  → λ(duplicate : ∀(b : Type) → g b → h (f b))
 6  → λ(a : Type)
 7  → λ(lan : ./Type f g a)
 8  → lan
 9    (h a)
10    (   λ(b : Type)
11      → λ(k : f b → a)
12      → λ(x : g b)
13      → functor.map (f b) a k (duplicate b x)
14    )