1    λ(f : Type → Type)
2  → λ(comonad : ./../Comonad/Type f)
3  → ./../Lan/lift f comonad f