let cat = ../Category/Cat/semigroupal

let vObject = Type

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

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