1    λ(f : Type → Type)
2  → λ(functor : ./../Functor/Type f)
3  → ./../Ran/lift f functor ./../Identity/Type f (λ(a : Type) → λ(x : f a) → x)