let cat = ../Category/Cat/semigroupal

let vObject = Type

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

let vBase = ../Category/Monoidal/extractCategory cat Type vObject v

let Category = ../Category/Kind cat vObject

in  λ(cObject : Kind) →
    λ(c : Category cObject) →
    λ(dObject : Kind) →
    λ(d : Category dObject) →
    λ(dCategory : ../Category/Type dObject v d) →
    λ(f : cat.arrow cObject dObject) →
    λ(functor : ../Functor/Type vObject cObject dObject vBase c d f) →
      ../Ran/lift
        cObject
        cObject
        dObject
        c
        d
        (../Category/extractSemigroupoid dObject v d dCategory)
        f
        functor
        (../Identity/Type cObject)
        f
        (λ(a : cObject) → dCategory.unit (f a))