1    λ(f : Type → Type)
 2  → λ(g : Type → Type)
 3  →   { map =
 4            λ(a : Type)
 5          → λ(b : Type)
 6          → λ(h : a → b)
 7          → λ(ran : ./Type f g a)
 8          → λ(c : Type)
 9          → λ(k : b → f c)
10          → ran c (λ(x : a) → k (h x))
11      }
12    : ./../Functor/Type (./Type f g)