λ(cat : ../Monoidal/Sort) →
λ(vObject : Kind) →
λ(object : Kind) →
λ(rig : ./Kind cat vObject object) →
      { unit = rig.additive.unit, product = rig.additive.product }
    ∧ ./extractCategory cat vObject object rig
  : ../Monoidal/Kind cat vObject object