let cat = ../../Category/Cat/semigroupal

let vObject = Type

let MonoidalCategory = ../../Category/Monoidal/Kind cat vObject

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

      in  λ(d : MonoidalCategory dObject) →
          λ(f : cat.arrow cObject dObject) →
          λ(monoidal : ./Type cObject v c d f) →
            let base = ../../Category/Monoidal/extractCategory cat vObject

            in    monoidal.{ map }
                : ../../Functor/Type
                    vObject
                    cObject
                    dObject
                    v
                    (base cObject c)
                    (base dObject d)
                    f