-- Monoid STRUCTURE on a small carrier, as a 𝕌-family: IsMonoid M is a
-- CODE packaging the operation, the unit and the laws, so it can sit
-- inside other codes (IsGroup and IsField layer it directly) and be
-- passed around as data. What makes this possible is Core/id.nova's Id:
-- the Ω-valued ≡ has no code, but its structural counterpart Id does,
-- and the two are logically equivalent (idToEq/eqToId) — so laws
-- stated with Id lose nothing, and instances convert the corpus's
-- ≡-lemmas componentwise via eqToId.
--
-- Law orientations follow the corpus's conventions (plusAssoc,
-- zeroPlusId, plusZeroId): assoc reassociates to the right, units
-- cancel toward the bare element.
import Core.id (Id)
IsMonoid : 𝕌 → 𝕌
IsMonoid =
λM. (op : M → M → M)
(e : M)
(assoc : (x y z : M) → Id _ (op (op x y) z) (op x (op y z)))
(unitL : (x : M) → Id _ (op e x) x)
× (x : M) → Id _ (op x e) x