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) →
              monoidal.{ unit, product }
            : ../../Monoid/Type
                (cat.arrow cObject dObject)
                (../../Category/Functor/monoidal cObject v c d)
                f