Classical.Structures.Monoid¶
Monoids¶
This is the Classical.Structures.Monoid module of the Agda Universal Algebra Library.
A monoid inhabits the Σ-typed structure Σ[ 𝑨 ∈ Algebra α ρ ] 𝑨 ⊨ Th-Monoid over Sig-Monoid.
Monoid is the first structure whose signature genuinely grows over its predecessor's
(Sig-Monoid adds ε-Op to Sig-Magma), and consequently the first whose forgetful
projection is not proj₁ but a true reduct.
This module's prose is normative for every later signature-growing structure (Group, Ring, etc.); the conventions it adds to the Semigroup template are as follows.
-
Direct curried accessors, not inherited-through-the-forgetful. Where
Semigroup-Opre-exported_∙_fromMagma-Op (semigroup→magma 𝑺)— sound because that forgetful functor isproj₁, so the magma's∙is the semigroup's∙definitionally —Monoid-Opdefines_∙_ = Curry₂ (∙-Op ^ 𝑨)andε = Curry₀ (ε-Op ^ 𝑨)directly overSig-Monoid; the reductmonoid→magmare-indexes arguments through the container morphism's position map, so the reduct's∙agrees with the monoid's only up to that map's reduction; defining the accessors directly keeps every downstreamrefloff that bet; each later signature-growing structure follows suit. -
Curried laws factored out above the forgetful. The curried associativity
mn-associs proved once, standalone, beforemonoid→semigroup, because the forgetful'sTh-Semigroupobligation consumes it;Monoid-Op.assoc-lawthen re-exposes the samemn-assoc, so there is a single proof of curried associativity, with a single proof; the acyclic ordering ismn-assoc→Monoid-Op.assoc-law(=mn-assoc 𝑴) →monoid→semigroup(which opensMonoid-Opforassoc-law). - The forgetful is a reduct.
monoid→semigroupreducts theSig-Monoid-algebra to aSig-Magma-algebra (droppingε-Opvia the container morphism∙-incl) and dischargesTh-Semigroupfrommn-assocby the curried-law pivot — the monoid's curried associativity transfers to the reduct verbatim (reduct preserves carrier,≈, and∙), and is re-inflated to the reduct'sSig-Magmaassociativity terms by the reduct's owninterp-node∙; no reduct-preserves-satisfaction term machinery is needed; see ADR-002 v2 §5, §9.
The local satisfaction predicate¶
infix 4 _⊨ᵐᵒ_ _⊨ᵐᵒ_ : (𝑨 : Algebra α ρ) (ℰ : Eq-Monoid → Term (Fin 3) × Term (Fin 3)) → Type (α ⊔ ρ) 𝑨 ⊨ᵐᵒ ℰ = ∀ i → 𝑨 ⊧ proj₁ (ℰ i) ≈ proj₂ (ℰ i)
The type of monoids¶
Monoid : (α ρ : Level) → Type (suc α ⊔ suc ρ) Monoid α ρ = Σ[ 𝑨 ∈ Algebra α ρ ] 𝑨 ⊨ᵐᵒ Th-Monoid
The reduct to magmas¶
The container morphism Sig-Magma ⟹ Sig-Monoid sends the magma's ∙-Opᵐᵃ to the
monoid's ∙-Op; the position map is the identity (Fin 2 to Fin 2).
monoid→magma is the induced reduct of the underlying algebra.
∙-incl : Op-Magma → Op-Monoid ∙-incl ∙-Opᵐᵃ = ∙-Op ∙-κ : (o : OperationSymbolsOf Sig-Magma) → ArityOf Sig-Monoid (∙-incl o) → ArityOf Sig-Magma o ∙-κ ∙-Opᵐᵃ = λ z → z
With that:
monoid→magma : Monoid α ρ → Magma α ρ monoid→magma 𝑴 = reductBy ∙-incl ∙-κ (𝑴 .proj₁)
Curried associativity, standalone¶
mn-assoc proves (x ∙ y) ∙ z ≈ x ∙ (y ∙ z) for the monoid's own ∙, from
equations assoc, via the local binary node-bridge interp-node∙ built on
IntMo.interp-cong. It is defined here, above the forgetful, so both
monoid→semigroup and Monoid-Op.assoc-law can consume it. The proof is a
verbatim port of Semigroup-Op.assoc-law to Sig-Monoid.
module _ (𝑴 : Monoid α ρ) where private 𝑨 = proj₁ 𝑴 open Setoid 𝔻[ 𝑨 ] using (_≈_; sym) renaming (refl to ≈refl) open Environment 𝑨 using ( ⟦_⟧ ) open SetoidReasoning 𝔻[ 𝑨 ] private infixl 7 _∙_ _∙_ : 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] _∙_ = Curry₂ (∙-Op ^ 𝑨) interp-node∙ : (s t : Term (Fin 3)) (η : Fin 3 → 𝕌[ 𝑨 ]) → ⟦ node ∙-Op (pair s t) ⟧ ⟨$⟩ η ≈ (⟦ s ⟧ ⟨$⟩ η) ∙ (⟦ t ⟧ ⟨$⟩ η) interp-node∙ s t η = interp-cong 𝑨 ∙-Op (λ { 0F → ≈refl ; 1F → ≈refl }) mn-assoc : ∀ x y z → x ∙ y ∙ z ≈ x ∙ (y ∙ z) mn-assoc x y z = begin x ∙ y ∙ z ≈˘⟨ interp-cong 𝑨 ∙-Op (λ { 0F → interp-node∙ (ℊ 0F) (ℊ 1F) η ; 1F → ≈refl }) ⟩ ⟦ lhsT ⟧ ⟨$⟩ η ≈⟨ proj₂ 𝑴 assoc η ⟩ ⟦ rhsT ⟧ ⟨$⟩ η ≈⟨ interp-cong 𝑨 ∙-Op (λ { 0F → ≈refl ; 1F → interp-node∙ (ℊ 1F) (ℊ 2F) η }) ⟩ x ∙ (y ∙ z) ∎ where η : Fin 3 → 𝕌[ 𝑨 ] η = λ { 0F → x ; 1F → y ; 2F → z } lhsT rhsT : Term (Fin 3) lhsT = node ∙-Op (pair (node ∙-Op (pair (ℊ 0F) (ℊ 1F))) (ℊ 2F)) rhsT = node ∙-Op (pair (ℊ 0F) (node ∙-Op (pair (ℊ 1F) (ℊ 2F))))
The Monoid-Op module¶
module Monoid-Op {α ρ : Level} (𝑴 : Monoid α ρ) where private 𝑨 = proj₁ 𝑴 open Setoid 𝔻[ 𝑨 ] using (_≈_; trans; sym) renaming (refl to ≈refl) open Environment 𝑨 using ( ⟦_⟧ ) infixl 7 _∙_ _∙_ : 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] → 𝕌[ 𝑨 ] _∙_ = Curry₂ (∙-Op ^ 𝑨) ε : 𝕌[ 𝑨 ] ε = Curry₀ (ε-Op ^ 𝑨) equations : 𝑨 ⊨ᵐᵒ Th-Monoid equations = proj₂ 𝑴 ∙-cong : ∀ {x y u v} → x ≈ y → u ≈ v → x ∙ u ≈ y ∙ v ∙-cong x≈y u≈v = interp-cong 𝑨 ∙-Op (λ { 0F → x≈y ; 1F → u≈v }) interp-node-∙ : (s t : Term (Fin 3)) {η : Fin 3 → 𝕌[ 𝑨 ]} → ⟦ node ∙-Op (pair s t) ⟧ ⟨$⟩ η ≈ ⟦ s ⟧ ⟨$⟩ η ∙ ⟦ t ⟧ ⟨$⟩ η interp-node-∙ s t = interp-cong 𝑨 ∙-Op (λ { 0F → ≈refl ; 1F → ≈refl }) interp-node-ε : {η : Fin 3 → 𝕌[ 𝑨 ]} → ⟦ node ε-Op (λ ()) ⟧ ⟨$⟩ η ≈ ε interp-node-ε = interp-cong 𝑨 ε-Op (λ ()) assoc-law : ∀ x y z → x ∙ y ∙ z ≈ x ∙ (y ∙ z) assoc-law = mn-assoc 𝑴 idˡ-law : ∀ x → ε ∙ x ≈ x idˡ-law x = trans (∙-cong (sym interp-node-ε) ≈refl) (trans (sym (interp-node-∙ (node ε-Op (λ ())) (ℊ 0F))) (equations idˡ (λ _ → x))) idʳ-law : ∀ x → x ∙ ε ≈ x idʳ-law x = trans (∙-cong ≈refl (sym (interp-node-ε))) (trans (sym (interp-node-∙ (ℊ 0F) (node ε-Op (λ ())))) (equations idʳ (λ _ → x)))
The forgetful projection to semigroups¶
monoid→semigroup : Monoid α ρ → Semigroup α ρ monoid→semigroup ℳ@(𝑴 , _) = 𝑹 , thm where 𝑹 : Magma _ _ 𝑹 = monoid→magma ℳ open Algebra 𝑴 using () renaming (Domain to M) open Setoid M using (_≈_; sym) renaming (refl to ≈refl) open Environment 𝑹 using ( ⟦_⟧ ) -- Sig-Magma environment on 𝑹 open SetoidReasoning M open Magma-Op 𝑹 using ( _∙_ ) -- 𝑹's curried ∙, over Sig-Magma -- 𝑹's binary node-bridge, over Sig-Magma interp-congᴿ : (s t : Term (Fin 3)) (η : Fin 3 → 𝕌[ 𝑴 ]) → ⟦ node ∙-Opᵐᵃ (pair s t) ⟧ ⟨$⟩ η ≈ (⟦ s ⟧ ⟨$⟩ η) ∙ (⟦ t ⟧ ⟨$⟩ η) interp-congᴿ s t η = interp-cong 𝑹 ∙-Opᵐᵃ λ { 0F → ≈refl ; 1F → ≈refl } -- 𝑹's curried-∙ congruence ∙-congᴿ : ∀ {a b c d} → a ≈ b → c ≈ d → (a ∙ c) ≈ (b ∙ d) ∙-congᴿ a≈b c≈d = interp-cong 𝑹 ∙-Opᵐᵃ (λ { 0F → a≈b ; 1F → c≈d }) thm : 𝑹 ⊨ˢᵍ Th-Semigroup thm assocˢ η = begin ⟦ Th-Semigroup assocˢ .proj₁ ⟧ ⟨$⟩ η ≈⟨ interp-congᴿ xy (ℊ 2F) η ⟩ ⟦ xy ⟧ ⟨$⟩ η ∙ z ≈⟨ ∙-congᴿ (interp-congᴿ (ℊ 0F) (ℊ 1F) η) ≈refl ⟩ x ∙ y ∙ z ≈⟨ assoc-law x y z ⟩ x ∙ (y ∙ z) ≈˘⟨ ∙-congᴿ ≈refl (interp-congᴿ (ℊ 1F) (ℊ 2F) η) ⟩ x ∙ ⟦ yz ⟧ ⟨$⟩ η ≈˘⟨ interp-congᴿ (ℊ 0F) yz η ⟩ ⟦ Th-Semigroup assocˢ .proj₂ ⟧ ⟨$⟩ η ∎ where open Monoid-Op ℳ using ( assoc-law ) -- the monoid's curried associativity x y z : 𝕌[ 𝑴 ] x = η 0F ; y = η 1F ; z = η 2F xy yz : Term (Fin 3) xy = node ∙-Opᵐᵃ (pair (ℊ 0F) (ℊ 1F)) -- the subterm x ∙ y yz = node ∙-Opᵐᵃ (pair (ℊ 1F) (ℊ 2F)) -- the subterm y ∙ z
The statement is 𝑹 ⊧ (Sig-Magma assoc-lhs) ≈ (Sig-Magma assoc-rhs) under every η,
and the proof is the curried-law pivot: unfold both Sig-Magma terms to the reduct's
curried ∙ᴿ via IntMa.interp-cong 𝑹 ∙-Opᵐᵃ, apply mn-assoc 𝑴 (whose ∙ is that
of the monoid, definitionally equal to ∙ᴿ since the position map is id), then
refold. Mechanically identical to Semigroup-Op.assoc-law but on 𝑹 and pivoting
through mn-assoc 𝑴 in the middle.
Homomorphism invariants¶
Per the policy stated in Classical.Structures.Magma, morphism invariants are
theorems about the inherited Sig-Monoid-homomorphisms, not new record fields. The
inaugural instance is the one that prose names explicitly: homomorphisms preserve
the identity element. The proof needs only the homomorphism's compatibility at
ε-Op — no monoid theory — so it is stated for raw Sig-Monoid-algebras, in the
curried form (Curry₀ (ε-Op ^ 𝑨) is the distinguished element of 𝑨) that
downstream consumers use; the empty-arity tuple bridge is one interp-cong with the
vacuous pointwise witness λ ().
module _ {α β ρᵃ ρᵇ : Level} {𝑨 : Algebra {𝑆 = Sig-Monoid} α ρᵃ} {𝑩 : Algebra {𝑆 = Sig-Monoid} β ρᵇ} where open Setoid 𝔻[ 𝑩 ] using () renaming ( _≈_ to _≈ᵇ_ ; trans to ≈ᵇ-trans ) -- Monoid homomorphisms preserve the identity element: h ε ≈ ε. hom-preserves-ε : (h : hom 𝑨 𝑩) → proj₁ h ⟨$⟩ Curry₀ (ε-Op ^ 𝑨) ≈ᵇ Curry₀ (ε-Op ^ 𝑩) hom-preserves-ε h = ≈ᵇ-trans (IsHom.compatible (proj₂ h) {ε-Op} {λ ()}) (interp-cong 𝑩 ε-Op (λ ()))
Monoid Builders¶
opsToBareMonoid builds a "raw" algebra in the signature of a monoid from a carrier,
a binary operation, and an identity element. It is opsToMagma followed by one
expand-ε, building the magma over ≡.setoid A and adjoining e as the
interpretation of ε-Op.
opsToBareMonoid : {A : Type α} (_·_ : A → A → A) (e : A) → Algebra {𝑆 = Sig-Monoid} α α opsToBareMonoid {A = A} _·_ e = expand-ε e where open Algebra 𝑩 : Algebra {𝑆 = Sig-Magma} _ _ 𝑩 = opsToMagma _·_ -- expand-ε interprets ε-Op as a *chosen element of the existing carrier* — it is a -- section of the reduct along Sig-Magma ↪ Sig-Monoid (opsToBareMonoid-section -- below), not the reduct's left adjoint. The *free* expansion, which adjoins a -- fresh element and is universal, is Classical.Categories.AdjoinUnit (M4-5d); see -- docs/notes/m4-5d-free-expansion.md for the comparison. expand-ε stays inline; -- a shared `expand` module is still deferred until Group's expand-⁻¹ provides a -- second consumer. expand-ε : A → Algebra {𝑆 = Sig-Monoid} _ _ expand-ε _ .Domain = 𝔻[ 𝑩 ] expand-ε _ .Interp ⟨$⟩ (∙-Op , args) = (∙-Opᵐᵃ ^ 𝑩) args expand-ε e .Interp ⟨$⟩ (ε-Op , _) = e expand-ε _ .Interp .cong {∙-Op , _} {.∙-Op , _} (refl , u≈v) = cong (𝑩 .Interp) (refl , u≈v) expand-ε _ .Interp .cong {ε-Op , _} {.ε-Op , _} (refl , _) = Setoid.refl 𝔻[ 𝑩 ]
That expand-ε is a section of the reduct — reducting the expansion recovers the
original magma, carrier and interpretation on the nose — is a definitional fact,
recorded here in the strict operation-level form of
Setoid.Algebras.Reduct's functoriality laws. This is the formal half of
the section-versus-adjoint contrast of M4-5d: expand-ε chooses an existing
element to interpret ε-Op (so the carrier is unchanged and the reduct round-trips),
whereas the free expansion adjoinUnit of Classical.Categories.AdjoinUnit
adjoins a fresh element (enlarging the carrier) and is universal.
opsToBareMonoid-section : {A : Type α} (_·_ : A → A → A) (e : A) (o : OperationSymbolsOf Sig-Magma) → o ^ reductBy ∙-incl ∙-κ (opsToBareMonoid _·_ e) ≡ o ^ opsToMagma _·_ opsToBareMonoid-section _·_ e ∙-Opᵐᵃ = refl
eqsToMonoid builds a Monoid by first building the raw algebra via opsToBareMonoid,
then proving the monoid laws from the given equations. The proof is a verbatim port
of Semigroup-Op.assoc-law to Sig-Monoid for associativity, and straightforward
for the identity laws.
eqsToMonoid : {A : Type α} (_·_ : A → A → A) (e : A) → (·-assoc : ∀ a b c → (a · b) · c ≡ a · (b · c)) → (·-idˡ : ∀ a → e · a ≡ a) (·-idʳ : ∀ a → a · e ≡ a) → Monoid α α eqsToMonoid _·_ e ·-assoc ·-idˡ ·-idʳ = opsToBareMonoid _·_ e , proof where proof : opsToBareMonoid _·_ e ⊨ᵐᵒ Th-Monoid proof assoc ρ = ·-assoc (ρ 0F) (ρ 1F) (ρ 2F) proof idˡ ρ = ·-idˡ (ρ 0F) proof idʳ ρ = ·-idʳ (ρ 0F)