λ(cat : ../Category/Semigroupal/Sort) →
λ(m : Kind) →
  { product : cat.arrow (cat.product m m) m }