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) →
            let base = ../../Category/Monoidal/extractCategory cat vObject

            in    ../Type
                    vObject
                    cObject
                    dObject
                    v
                    (base cObject c)
                    (base dObject d)
                    f
                ⩓ ../../Monoid/Type
                    (cat.arrow cObject dObject)
                    (../../Category/Functor/monoidal cObject v c d)
                    f