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

in  λ(cObject : Kind) →
    λ(c : ../../Category/Kind cat vObject cObject) →
    λ(cSemigroupoid : ../../Semigroupoid/Type cObject v c c.arrow) →
      let dObject = Type

      let d =
            ../../Category/Monoidal/Cartesian/extractCategory
              cat
              vObject
              dObject
              ../../Category/Set/monoidal/cartesian

      in  λ(f : cat.arrow cObject dObject) →
              ../../Ran/functor
                cObject
                cObject
                c
                cSemigroupoid
                (../../Identity/Type cObject)
                f
            : ../../Functor/Type
                vObject
                cObject
                dObject
                vBase
                c
                d
                (../Type cObject c f)