let kCat = ../Category/Cat/semigroupal

let base = ../Category/Monoidal/Cartesian/extractCategory kCat

let vObject = Type

let v = base Type vObject ../Category/Set/monoidal/cartesian

let object = Type

let cat = base vObject object ../Category/Set/monoidal/cartesian

in  λ(f : kCat.arrow object object) →
    λ(functor : ../Functor/Endo/Type vObject object v cat f) →
    λ(comonad : ../Comonad/Type object cat f) →
      ../Lan/lower object object cat f functor f f comonad.product