{-|
A duoid (also known as a “united monoid”) is actually a pair of monoids with a
shared `unit`.
-}
λ(cat : ../Category/Monoidal/Sort) →
λ(m : Kind) →
  { diamond : ../Semilattice/Bounded/Kind cat m, star : ../Monoid/Kind cat m }