Skip to content

Classical.Theories.Semigroup

The equational theory of semigroups

This is the Classical.Theories.Semigroup module of the Agda Universal Algebra Library.

This is the first concrete equational theory module in the Classical/ tree, and as such this file's prose is normative for every subsequent Classical/Theories/X.lagda.md (Monoid in M3-6, Group in M3-6, Lattice in M3-7, Ring in M3-8). See ADR-002 v2 ยง3, ยง4 for the design rationale.

The shape established here is:

  • An index type Eq-<Structure> : Type โ€” a small named enum whose constructors correspond one-to-one with the defining equations of <Structure>'s theory. For semigroups the index is the singleton enum Eq-Semigroup with sole constructor assoc. Single-equation theories use a singleton enum rather than degenerating the index to โŠค; the named constructor pays for itself in error-message readability and in symmetry with multi-equation theories landing later.
  • A theory function Th-<Structure> : Eq-<Structure> โ†’ Term (Fin n) ร— Term (Fin n) composed from the generic equation builders of Classical.Equations (M3-2) applied to the operation symbols of Sig-<Structure>. The codomain is spelled in its long form rather than abbreviated to _, per the meta-resolution-pitfall note in ADR-002 v2 ยง4.
  • The variable carrier is Fin n for the smallest n that suffices, per ADR-002 v2 ยง2. Associativity needs three distinct variables, so n = 3 and the variable patterns at use sites are 0F, 1F, 2F from Data.Fin.Patterns.

Since semigroups share the magma signature Sig-Magma โ€” semigroups are precisely those magmas whose binary operation is associative โ€” there is no Sig-Semigroup. The variable carrier Fin 3 and the magma signature Sig-Magma together fully parameterize the equation builder Associative from Classical.Equations.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Classical.Theories.Semigroup where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Agda.Primitive                         using () renaming ( Set to Type )
open import Data.Fin.Base                          using ( Fin )
open import Data.Fin.Patterns                      using ( 0F ; 1F ; 2F )
open import Data.Product                           using ( _ร—_ )
open import Relation.Binary.PropositionalEquality  using ( refl )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Classical.Signatures.Magma             using ( Sig-Magma ; โˆ™-Op )
open import Classical.Equations                    using ( Associative )
open import Overture.Terms {๐‘† = Sig-Magma}         using ( Term )

The index of equations

Semigroup's theory has exactly one equation, associativity. The singleton enum Eq-Semigroup names it.

data Eq-Semigroup : Type where
  assoc : Eq-Semigroup

The theory map

Th-Semigroup sends the sole equation constructor assoc to the associativity term-pair built by the generic Associative builder from Classical.Equations. The arity-conformance evidence refl typechecks because ar-Magma โˆ™-Op reduces definitionally to Fin 2 โ€” this is what the Classical/Signatures/Magma arity-function-by-direct-pattern-matching convention buys us.

Th-Semigroup : Eq-Semigroup โ†’ Term (Fin 3) ร— Term (Fin 3)
Th-Semigroup assoc = Associative โˆ™-Op refl 0F 1F 2F

Unfolded, Th-Semigroup assoc is the pair ((โ„Š 0F โˆ™ โ„Š 1F) โˆ™ โ„Š 2F , โ„Š 0F โˆ™ (โ„Š 1F โˆ™ โ„Š 2F)) of Sig-Magma-terms over the variable carrier Fin 3 โ€” the left-associated and right-associated three-fold product, respectively.