let cat = ../Category/Cat/semigroupal

let vObject = Type

let v =
      ../Category/Monoidal/Cartesian/extractMonoidal
        cat
        Type
        vObject
        ../Category/Set/monoidal/cartesian

in  λ(cObject : Kind) →
      let dObject = Type

      in  λ(d : ../Category/Kind cat vObject dObject) →
          λ(dSemigroupoid : ../Semigroupoid/Type dObject v d d.arrow) →
          λ(f : cat.arrow cObject dObject) →
            ../Lan/functor cObject dObject d dSemigroupoid f f