Classical.Structures.CommutativeSemigroup¶

Commutative Semigroups¶

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

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

This is an equation-only extension of an equation-bearing predecessor; the forgetful projection of such an extension is a pure theory reindex (the algebra is kept; the satisfaction proof is restricted to the predecessor's equations), so the predecessor's <Weaker>-Op accessors go through unchanged. CommutativeSemigroup-Op adds only the new curried comm-law.¹

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

module Classical.Structures.CommutativeSemigroup 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.Magma               using  ( Sig-Magma )
open import Classical.Structures.Magma               using  ( opsToMagma )
open import Classical.Structures.Semigroup           using  ( Semigroup ; module Semigroup-Op )
open import Classical.Theories.Semigroup             using  ( assoc )
open import Classical.Theories.CommutativeSemigroup  using  ( Eq-CommutativeSemigroup
                                                            ; Th-CommutativeSemigroup ; comm )
                                                     renaming ( assoc to assocᶜ )
open import Overture.Terms {𝑆 = Sig-Magma}           using  (Term ; ℊ )
open import Setoid.Algebras.Basic    using  ( Algebra ; 𝔻[_] ; 𝕌[_] )
open import Setoid.Varieties.EquationalLogic using ( _⊧_≈_ )

private variable α ρ : Level

Satisfaction predicate and the type¶

infix 4 _⊨ᶜˢᵍ_
_⊨ᶜˢᵍ_ : (𝑨 : Algebra {𝑆 = Sig-Magma} α ρ) (ℰ : Eq-CommutativeSemigroup → Term (Fin 3) × Term (Fin 3)) → Type (α ⊔ ρ)
𝑨 ⊨ᶜˢᵍ ℰ = ∀ i → 𝑨 ⊧ proj₁ (ℰ i) ≈ proj₂ (ℰ i)

CommutativeSemigroup : (α ρ : Level) → Type (suc α ⊔ suc ρ)
CommutativeSemigroup α ρ = Σ[ 𝑨 ∈ Algebra {𝑆 = Sig-Magma} α ρ ] 𝑨 ⊨ᶜˢᵍ Th-CommutativeSemigroup

The forgetful projection to semigroups (pure reindex)¶

The pattern assoc is Eq-Semigroup's sole constructor; the applied assocᶜ is Eq-CommutativeSemigroup's (renamed on import). Both theory entries are Associative ∙-Op refl 0F 1F 2F, hence definitionally equal, so the reindex checks.

commutativeSemigroup→semigroup : CommutativeSemigroup α ρ → Semigroup α ρ
commutativeSemigroup→semigroup (𝑨 , mod) = 𝑨 , λ { assoc → mod assocᶜ }

The `CommutativeSemigroup-Op` module¶

CommutativeSemigroup-Op 𝑪 re-exports the semigroup interface — _∙_, ∙-cong, interp-node and assoc-law — through the forgetful, and adds equations, the satisfaction witness, together with comm-law.

Note which containment lemma is inherited here: this structure sits over Sig-Magma, whose single binary symbol needs only the one interp-node, where the monoid line has a separate lemma per operation symbol. comm-law then reads equations comm between two applications of it.

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

  -- Inherit through the (proj₁-on-algebra) reindex forgetful.
  open Semigroup-Op (commutativeSemigroup→semigroup 𝑪) public
    using ( _∙_ ; ∙-cong ; interp-node ; assoc-law )

  equations : 𝑨 ⊨ᶜˢᵍ Th-CommutativeSemigroup
  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 3 → 𝕌[ 𝑨 ]
          η = λ { 0F → x ; 1F → y ; 2F → x }

`eqsToCommutativeSemigroup`¶

eqsToCommutativeSemigroup builds a commutative semigroup from a carrier, a binary operation, and propositional associativity and commutativity. It factors through opsToMagma — not opsToBareMonoid, since there is no identity element to supply — and both obligations reduce definitionally, so each is the given law read off at the environment components.

eqsToCommutativeSemigroup : (A : Type α) (_·_ : A → A → A)
  → (·-assoc : ∀ a b c → (a · b) · c ≡ a · (b · c))
  → (·-comm  : ∀ a b → a · b ≡ b · a)
  → CommutativeSemigroup α α
eqsToCommutativeSemigroup A _·_ ·-assoc ·-comm = opsToMagma _·_ , proof
  where
  proof : opsToMagma _·_ ⊨ᶜˢᵍ Th-CommutativeSemigroup
  proof assocᶜ ρ = ·-assoc (ρ 0F) (ρ 1F) (ρ 2F)
  proof comm   ρ = ·-comm  (ρ 0F) (ρ 1F)

See ADR-002 v2 §5. ↩