let kCat = ../Cat/semigroupal

let vObject = Type

in  λ(object : Kind) →
    λ(v : ../Monoidal/Kind kCat Type vObject) →
    λ(cat : ./Kind kCat vObject object) →
    λ(rig : ./Type object v cat) →
        rig.multiplicative
      : ../Monoidal/Type
          object
          v
          (./extractMultiplicative kCat vObject object cat)