Examples.Classical.Semigroup

Worked example: (ℕ, +) as a semigroup

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

The natural numbers under addition form the canonical first semigroup to exhibit, mirroring the magma example in Examples.Classical.Magma. Beyond demonstrating that the M3-4 deliverable type-checks, this module is the home for all future semigroup-specific worked examples: alternative semigroups on ℕ, finite semigroups, the free semigroup over a generating set, semigroups that fail to be monoids, and so on. Subsequent additions should land here rather than alongside the core structure file.

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

module Examples.Classical.Semigroup where

-- Imports from Agda and the Agda Standard Library ----------------------------
open import Data.Nat                               using ( ℕ ; _+_ )
open import Data.Nat.Properties                    using ( +-assoc )
open import Relation.Binary.PropositionalEquality  using ( _≡_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import Classical.Bundles.Semigroup           using ( ⟨_⟩ˢᵍ ; ⟪_⟫ˢᵍ )
open import Classical.Small.Structures.Semigroup  using ( Semigroup ; eqsToSemigroup )
open import Examples.Classical.Magma              using ( ℕ-magma )

import Classical.Structures.Semigroup as Polymorphic

The semigroup (ℕ, +)

We build (ℕ, +) directly from stdlib's +-assoc. The eqsToSemigroup constructor demands an associativity proof of exactly the shape ∀ a b c → (a + b) + c ≡ a + (b + c), which is the type of +-assoc up to the definitional equality Associative _+_ = ∀ x y z → (x + y) + z ≡ x + (y + z).

ℕ-semigroup : Semigroup
ℕ-semigroup = eqsToSemigroup ℕ _+_ +-assoc

open Polymorphic.Semigroup-Op ℕ-semigroup using ( _∙_ )

Acceptance checks

∙-Op interpreted in ℕ-semigroup reduces definitionally to _+_: no opacity from the eqsToSemigroup construction, from the factoring through opsToMagma, or from the Curry₂ wrapping in the inherited named accessor; discharged by refl.

∙-is-+-sg : ∀ (a b : ℕ) → a ∙ b ≡ a + b
∙-is-+-sg a b = refl

The forgetful image of ℕ-semigroup is the magma ℕ-magma on the nose. This holds because eqsToSemigroup is implemented as opsToMagma _·_ , <proof>, so semigroup→magma (eqsToSemigroup ℕ _+_ +-assoc) reduces to opsToMagma ℕ _+_, which is exactly the definition of ℕ-magma; discharged by refl.

forgetful-agrees : Polymorphic.semigroup→magma ℕ-semigroup ≡ ℕ-magma
forgetful-agrees = refl

The bundle bridge round-trips on ℕ-semigroup pointwise. Both directions reduce by pair a b 0F ⇉ a and pair a b 1F ⇉ b, so propositional refl discharges the obligation at the curried form (per ADR-002 v2 §6.

open Polymorphic.Semigroup-Op ⟪ ⟨ ℕ-semigroup ⟩ˢᵍ ⟫ˢᵍ using () renaming ( _∙_ to _·_ )

roundtrip-ℕ-sg : ∀ (a b : ℕ) → a · b ≡ a + b
roundtrip-ℕ-sg a b = refl