1    λ(w : Type → Type)
2  → λ(comonad : ./Type w)
3  → comonad.{ map } : ./../Functor/Type w