{-|
This is what is often called a “semiring”, but here we follow the convention
described in https://ncatlab.org/nlab/show/rig, reserving “semiring” for a rig
without multiplicative unit.
-}
λ(cat : ../Category/Monoidal/Sort) →
λ(m : Kind) →
  { additive : ../Monoid/Commutative/Kind cat m
  , multiplicative : ../Monoid/Kind cat m
  }