let kCat = ../Cat/semigroupal

let Category = ../Kind kCat

let MonoidalCategory = ../Monoidal/Kind kCat

let vObject = Type

in  λ(object : Kind) →
    λ(v : MonoidalCategory Type vObject) →
    λ(cat : Category vObject object) →
      let profunctor = kCat.arrow (kCat.product object object) vObject

      in  λ(morphism : profunctor) →
              { unit = morphism } ∧ ./semigroupal object v cat
            : MonoidalCategory vObject profunctor