let cat = ../Category/Cat/semigroupal

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

let vObject = Type

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

in  λ(cObject : Kind) →
    λ(c : ../Category/Kind cat vObject cObject) →
      let dCategory = ../Category/Set/category/instance

      let dObject = Type

      let d = base vObject dObject ../Category/Set/monoidal/cartesian

      in  λ(f : cat.arrow cObject dObject) →
          λ(functor : ../Functor/Type vObject cObject dObject v c d f) →
            ../Lan/lower
              cObject
              cObject
              c
              f
              functor
              (../Identity/Type cObject)
              f
              (λ(b : cObject) → dCategory.unit (f b))