1    λ(f : Type → Type)
2  → λ(comonad : ./../Comonad/Type f)
3  → ./../Lan/lower f (./../Comonad/extractFunctor f comonad) f f comonad.duplicate