λ(cat : ../Sort) →
λ(vObject : Kind) →
λ(object : Kind) →
λ(cartesian : ./Kind cat vObject object) →
    cartesian.{ constraint, arrow, product }
  : ../../Semigroupal/Kind cat vObject object