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