Skip to content

Examples.Setoid.Presentation

Worked example: a structure by generators and relations

This is the Examples.Setoid.Presentation module of the Agda Universal Algebra Library.

A presentation ⟨ X ∣ R ⟩ describes a structure by a set X of generators together with a set R of defining relations: the presented structure is the free algebra on X modulo the smallest congruence containing R. In the relatively-free-algebra machinery of Setoid.Varieties.SoundAndComplete this is exactly 𝔽[ X ] for the equation family R, whose carrier equality is derivable equality from R.

We take the smallest interesting presentation over the magma signature Sig-Magma: one generator a and one relation making it idempotent, ⟨ a ∣ a · a ≈ a ⟩ — the free band on one generator. Idempotence forces every nonempty product of a to collapse to a; we derive two instances of that collapse from the single defining relation.

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

module Examples.Setoid.Presentation 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 )

-- Imports from the Agda Universal Algebra Library -----------------------------
open import Classical.Signatures.Magma           using ( Sig-Magma ; ∙-Op )
open import Overture.Terms       {𝑆 = Sig-Magma} using ( Term ; ℊ ; node )
open import Setoid.Algebras      {𝑆 = Sig-Magma} using ( 𝔻[_] )
open import Setoid.Varieties.SoundAndComplete {𝑆 = Sig-Magma}
  using ( Eq ; _≈̇_ ; _⊨_ ; _⊢_▹_≈_ ; module FreeAlgebra )

open import Relation.Binary using ( Setoid )

open _⊢_▹_≈_ using ( hyp ; app ; refl ; trans )

The presentation ⟨ a ∣ a · a ≈ a ⟩

The single generator is a = ℊ 0F in the one-variable context Fin 1; the single relation is idempotence.

_·_ : {X : Type} → Term X → Term X → Term X
s · t = node ∙-Op λ { 0F → s ; 1F → t }

-- the sole generator
a : Term (Fin 1)
a = ℊ 0F

-- the sole relation:  a · a  ≈̇  a
idem-rel : Eq
idem-rel = (a · a) ≈̇ a

R : Fin 1 → Eq
R _ = idem-rel

open FreeAlgebra R using ( 𝔽[_] )

The presented structure is 𝔽[ Fin 1 ]; it models its own defining relation by construction.

presented-is-idempotent : 𝔽[ Fin 1 ] ⊨ R
presented-is-idempotent = FreeAlgebra.satisfies R

Consequences of the presentation

The carrier equality of 𝔽[ Fin 1 ] is derivable equality, so the defining relation is available as hyp 0F. Rewriting the redex a · a with congruence (app) and then once more at the top collapses the two three-fold products to a.

open Setoid 𝔻[ 𝔽[ Fin 1 ] ] using ( _≈_ )

-- the defining relation itself
idem : (a · a) ≈ a
idem = hyp 0F

-- (a · a) · a ≈ a   :  reduce the left factor, then the top
collapseˡ : ((a · a) · a) ≈ a
collapseˡ = trans (app λ { 0F → hyp 0F ; 1F → refl }) (hyp 0F)

-- a · (a · a) ≈ a   :  reduce the right factor, then the top
collapseʳ : (a · (a · a)) ≈ a
collapseʳ = trans (app λ { 0F → refl ; 1F → hyp 0F }) (hyp 0F)