Natural.monoid

-- (ℕ, +, 0) is a monoid: the operations are data components, and each
-- law is an existing Natural.nova ≡-lemma carried across the Id bridge
-- by eqToId, with both sides spelled so the component types meet the
-- expected ones exactly.

import Natural (+, *, plusAssoc, zeroPlusId, plusZeroId, multAssoc, sucPlus)
import Core.id (eqToId)
import Algebra.monoid (IsMonoid)

natAddMonoid : IsMonoid ℕ using (Algebra.monoid.IsMonoid.unfold)
natAddMonoid =
  (,)
    (+)
    Z
    λx y z. eqToId _ _ (plusAssoc x y z)
    λx. eqToId _ _ (zeroPlusId x)
    λx. eqToId _ _ (plusZeroId x)

-- The unit laws for * at S Z. On the right the whole statement is a
-- δβ-computation (n * S Z unwinds through * and + to n); on the left
-- the elimination is stuck on n, so it is an induction.
multOneR : (n : ℕ) → n * S Z ≡ n using (Natural.*.eq, Natural.+.eq)
multOneR = λn. ⋆

oneMultL : (n : ℕ) → S Z * n ≡ n
  using (*.eq,
    hyp.rw,
    Natural.multZeroId,
    Natural.multZeroId.rw,
    sucPlus,
    sucPlus.rw,
    zeroPlusId,
    zeroPlusId.rw)
oneMultL = λn. ℕ-elim ⋆ (k ih. ⋆) n

-- (ℕ, *, 1) is a monoid.
natMulMonoid : IsMonoid ℕ using (Algebra.monoid.IsMonoid.unfold)
natMulMonoid =
  (,)
    (*)
    S Z
    λx y z. eqToId _ _ (multAssoc x y z)
    λx. eqToId _ _ (oneMultL x)
    λx. eqToId _ _ (multOneR x)