let kCat = ../Cat/semigroupal

let MonoidalCategory = ../Monoidal/Kind kCat

let base = ../Monoidal/extractCategory kCat

let vObject = Type

in  λ(object : Kind) →
    λ(v : MonoidalCategory Type vObject) →
    λ(cat : MonoidalCategory vObject object) →
    λ(m : object) →
        { category : ../Type object v (base vObject object cat) }
      ⩓ ../../Bimonoid/Type object cat m