let kCat = ../Cat/semigroupal

in  λ(vObject : Kind) →
    λ(object : Kind) →
    λ(cat : ../Semigroupal/Kind kCat vObject object) →
          { product = cat.product }
        ∧ ./Kind
            vObject
            object
            (../../Category/Semigroupal/extractCategory kCat vObject object cat)
      : ../Semigroupal/Kind kCat vObject object