let cat = ../Category/Cat/semigroupal

let c = ../Category/Set/monoidal/cartesian

let vObject = Type

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

let cObject = Type

in  λ(dObject : Kind) →
    λ(d : ../Category/Kind cat vObject dObject) →
    λ(f : cat.arrow cObject dObject) →
    λ ( functor
      : ./Type
          vObject
          cObject
          dObject
          v
          (../Category/Monoidal/Cartesian/extractCategory cat vObject cObject c)
          d
          f
      ) →
    λ(a : cObject) →
      functor.map a c.unit (λ(_ : a) → {=})