let kCat = ../../Category/Cat/semigroupal

let monoidalBase = ../../Category/Monoidal/Cartesian/extractMonoidal kCat

let base = ../../Category/Monoidal/extractCategory kCat

let vObject = Type

let v =
      base
        Type
        vObject
        (monoidalBase Type vObject ../../Category/Set/monoidal/cartesian)

let object = Type

let cat = monoidalBase vObject object ../../Category/Set/monoidal/cartesian

in  λ(m : kCat.arrow object object) →
      ../../Functor/Monoidal/extractFunctor
        object
        v
        cat
        cat
        (../Type object (base vObject object cat) m)
        (./monoidal m)