Classical.Structures.CommutativeMonoid

Commutative Monoids

This is the Classical.Structures.CommutativeMonoid module of the Agda Universal Algebra Library.

A commutative monoid is an inhabitant of the type Σ[ 𝑨 ∈ Algebra α ρ ] 𝑨 ⊨ Th-CommutativeMonoid, where Algebra is parameterized by the Sig-Monoid type.

This module naturally codifies a commutative monoid as an equational extension of Monoid; commutativeMonoid→monoid is a pure theory-reindex, and CommutativeMonoid-Op inherits _∙_, ε, and all three monoid laws through it, adding comm-law.

{-# OPTIONS --without-K --exact-split --safe #-}

module Classical.Structures.CommutativeMonoid where

open import Agda.Primitive                         using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Fin.Base                          using ( Fin )
open import Data.Fin.Patterns                      using ( 0F ; 1F ; 2F )
open import Data.Product                           using ( Σ-syntax ; _×_ ; _,_ ; proj₁ ; proj₂ )
open import Level                                  using ( Level ; _⊔_ ; suc )
open import Relation.Binary                        using ( Setoid )
open import Relation.Binary.PropositionalEquality  using ( _≡_ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Classical.Signatures.Monoid            using ( Sig-Monoid )
open import Classical.Structures.Monoid            using ( Monoid ; module Monoid-Op ; opsToBareMonoid )
open import Classical.Theories.Monoid              using ( assoc ; idˡ ; idʳ )
open import Classical.Theories.CommutativeMonoid   using ( Eq-CommutativeMonoid ; Th-CommutativeMonoid ; comm )
                                                   renaming ( assoc to assocᶜ ; idˡ to idˡᶜ ; idʳ to idʳᶜ )
open import Overture.Terms {𝑆 = Sig-Monoid}        using (Term ; ℊ )
open import Setoid.Algebras.Basic                  using ( Algebra ; 𝔻[_] ; 𝕌[_] )
open import Setoid.Varieties.EquationalLogic       using ( _⊧_≈_ )

private variable α ρ : Level

Satisfaction predicate and the CommutativeMonoid type

infix  _⊨ᶜᵐᵒ_

_⊨ᶜᵐᵒ_ : (𝑨 : Algebra {𝑆 = Sig-Monoid} α ρ) (ℰ : Eq-CommutativeMonoid → Term (Fin ) × Term (Fin )) → Type (α ⊔ ρ)
𝑨 ⊨ᶜᵐᵒ ℰ = ∀ i → 𝑨 ⊧ proj₁ (ℰ i) ≈ proj₂ (ℰ i)

CommutativeMonoid : (α ρ : Level) → Type (suc α ⊔ suc ρ)
CommutativeMonoid α ρ = Σ[ 𝑨 ∈ Algebra α ρ ] 𝑨 ⊨ᶜᵐᵒ Th-CommutativeMonoid

The forgetful projection to monoids

commutativeMonoid→monoid keeps the algebra and discards commutativity. Because a commutative monoid is a monoid with an extra equation rather than an extra operation, the signature does not change and no reduct is needed; what the function does is re-index the satisfaction witness, mapping each constructor of Eq-Monoid to its counterpart in Eq-CommutativeMonoid. The λ { assoc → mod assocᶜ ; … } clause is exactly that renaming, and it is the cheap case of the pattern: contrast monoid→semigroup of Classical.Structures.Monoid, which must reduct and re-prove.

commutativeMonoid→monoid : CommutativeMonoid α ρ → Monoid α ρ
commutativeMonoid→monoid (𝑨 , mod) =
  𝑨 , λ { assoc → mod assocᶜ ; idˡ → mod idˡᶜ ; idʳ → mod idʳᶜ }

The CommutativeMonoid-Op module

CommutativeMonoid-Op 𝑪 inherits the whole monoid interface (_∙_, ε, the congruence, both containment lemmas and all three laws) and adds exactly one accessor of its own. equations is the new satisfaction witness, and comm-law is commutativity in curried form.

That single addition is the point of the idiom: the inherited names are re-exported rather than restated, so opening this module gives the full monoid vocabulary plus commutativity, and the only proof written here is the one genuinely new law. Its proof also shows why the containment lemmas were worth naming: comm-law is equations comm with interp-node-∙ applied on each side.

module CommutativeMonoid-Op {α ρ : Level} (𝑪 : CommutativeMonoid α ρ) where
  private 𝑨 = proj₁ 𝑪
  open Setoid 𝔻[ 𝑨 ]

  open Monoid-Op (commutativeMonoid→monoid 𝑪) public
    using  ( _∙_ ; ε ; ∙-cong ; interp-node-∙ ; interp-node-ε
           ; assoc-law ; idˡ-law ; idʳ-law )

  equations : 𝑨 ⊨ᶜᵐᵒ Th-CommutativeMonoid
  equations = proj₂ 𝑪

  comm-law : ∀ x y → x ∙ y ≈ y ∙ x
  comm-law x y = trans (sym (interp-node-∙ (ℊ 0F) (ℊ 1F) {η}))
                       (trans (equations comm η) (interp-node-∙ (ℊ 1F) (ℊ 0F) {η}))
    where η : Fin  → 𝕌[ 𝑨 ]
          η = λ { 0F → x ; 1F → y ; 2F → x }

eqsToCommutativeMonoid

eqsToCommutativeMonoid is the constructor a downstream user calls. It takes the raw data (a carrier, a binary operation, an identity element) and the four laws as propositional equations, and returns a CommutativeMonoid α α.

The four proof obligations discharge by direct evaluation rather than by reasoning. Under ≡.setoid A the setoid equality is propositional equality, and the interpretation of each term in opsToBareMonoid reduces definitionally to the corresponding application of _·_, so each clause is just the supplied law applied to the right environment components. Factoring through opsToBareMonoid is also what makes the forgetful-agreement criterion of ADR-002 discharge by refl.

eqsToCommutativeMonoid : (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)
  → (·-comm : ∀ a b → a · b ≡ b · a)
  → CommutativeMonoid α α
eqsToCommutativeMonoid A _·_ e ·-assoc ·-idˡ ·-idʳ ·-comm = opsToBareMonoid _·_ e , proof
  where
  proof : opsToBareMonoid _·_ e ⊨ᶜᵐᵒ Th-CommutativeMonoid
  proof assocᶜ ρ = ·-assoc (ρ 0F) (ρ 1F) (ρ 2F)
  proof idˡᶜ   ρ = ·-idˡ   (ρ 0F)
  proof idʳᶜ   ρ = ·-idʳ   (ρ 0F)
  proof comm   ρ = ·-comm  (ρ 0F) (ρ 1F)