Skip to content

Examples.Setoid.HSPCommutativeMonoid

Worked example: Birkhoff's HSP theorem specialized to (β„•, +, 0)

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

Setoid.Varieties.HSP proves Birkhoff's variety theorem for an arbitrary class 𝒦 of algebras over an arbitrary signature. This module instantiates that theorem at the singleton class 𝒦₀ = { (β„•, +, 0) } over the monoid signature Sig-Monoid, reusing the commutative monoid β„•-commutativeMonoid of Examples.Classical.CommutativeMonoid as the generating algebra.

We record four facts about the variety V 𝒦₀ generated by (β„•, +, 0):

  • the generating algebra belongs to its own variety (β„•βˆˆV, from expansiveness of V);
  • every identity true in (β„•, +, 0) β€” in particular commutativity β€” is an identity of the whole variety (V-commutative, from identity preservation);
  • Birkhoff's theorem, specialized: every model of the equational theory of V 𝒦₀ lies in V 𝒦₀ (Birkhoff-β„•);
  • and its converse (Birkhoff-converse-β„•).
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Examples.Setoid.HSPCommutativeMonoid where


-- Imports from the Agda Standard Library --------------------------------------
open import Data.Fin.Base         using ( Fin )
open import Data.Fin.Patterns     using ( 0F ; 1F )
open import Data.Nat.Properties   using ( +-comm )
open import Data.Product          using ( proj₁ )
open import Level                 using ( 0β„“ ; Level ) renaming (suc to lsuc)
open import Relation.Unary        using ( Pred ; _∈_ )

-- Imports from the Agda Universal Algebra Library -----------------------------
open import Examples.Classical.CommutativeMonoid                using  ( β„•-commutativeMonoid )
open import Classical.Signatures.Monoid                         using  ( Sig-Monoid ; βˆ™-Op )
open import Overture.Terms {𝑆 = Sig-Monoid}                     using  ( Term ; β„Š ; node )
open import Setoid.Algebras {𝑆 = Sig-Monoid}                    using  ( Algebra )
open import Setoid.Varieties.Closure {𝑆 = Sig-Monoid}           using  ( V ; Vβ€² ; V-expaβ€² )
open import Setoid.Varieties.Preservation {𝑆 = Sig-Monoid}      using  ( V-id1 )
open import Setoid.Varieties.SoundAndComplete {𝑆 = Sig-Monoid}  using  ( _⊫_ ; ⊫-proof
                                                                       ; _β‰ˆΜ‡_ ; Mod ; Th )
open import Setoid.Varieties.HSP {𝑆 = Sig-Monoid}               using  ( Birkhoff
                                                                       ; Birkhoff-converse )

1β„“ 2β„“ : Level
1β„“ = lsuc 0β„“
2β„“ = lsuc 1β„“

The generating algebra and the singleton class

β„•-commutativeMonoid is a Ξ£-pair of a Sig-Monoid algebra and a proof that it satisfies the commutative-monoid equations; its first projection is the underlying (β„•, +, 0) setoid algebra.

𝑨₀ : Algebra 0β„“ 0β„“
𝑨₀ = proj₁ β„•-commutativeMonoid

-- the singleton class { 𝑨₀ }, as a one-constructor family.  With the explicit-class
-- V-expaβ€² the closure operators no longer need this shape to infer 𝒦; we keep the
-- data family because π’¦β‚€βŠ«comm (below) reads cleanly by matching its inβ‚€ constructor.
data 𝒦₀ : Pred (Algebra 0β„“ 0β„“) 1β„“ where
  inβ‚€ : 𝒦₀ 𝑨₀

π‘¨β‚€βˆˆπ’¦β‚€ : 𝑨₀ ∈ 𝒦₀
π‘¨β‚€βˆˆπ’¦β‚€ = inβ‚€

The variety Vβ€² 𝒦₀ generated by 𝑨₀. Because every universe in play here is 0β„“, we use Vβ€² β€” the common-case specialization of V that collapses its eight level parameters to those of the generating class β€” giving a single concrete predicate 𝕍 that the corollaries below can refer to without pinning any level by hand or leaving unsolved level metavariables.

𝕍 : Pred (Algebra 0β„“ 0β„“) 2β„“
𝕍 = Vβ€² 0β„“ 1β„“ 𝒦₀

Corollary 1: the generator lies in its own variety

V is expansive, so (β„•, +, 0) belongs to the variety it generates. We obtain the membership from V-expaβ€², the explicit-class form of expansiveness: the class 𝒦₀ is passed positionally, so nothing has to be inferred and the intermediate levels are pinned by unification with the Vβ€² goal 𝕍.

β„•βˆˆV : 𝑨₀ ∈ 𝕍
β„•βˆˆV = V-expaβ€² 0β„“ 1β„“ 𝒦₀ π‘¨β‚€βˆˆπ’¦β‚€

Corollary 2: the variety is commutative

Commutativity of (β„•, +, 0) is exactly +-comm: the term identity x Β· y β‰ˆ y Β· x holds under every environment. Since 𝒦₀ is the singleton { 𝑨₀ }, the class models this identity; identity preservation (V-id1) then lifts it to the whole variety.

-- the two sides of the commutativity identity, over two variables
xΒ·y yΒ·x : Term (Fin 2)
xΒ·y = node βˆ™-Op Ξ» { 0F β†’ β„Š 0F ; 1F β†’ β„Š 1F }
yΒ·x = node βˆ™-Op Ξ» { 0F β†’ β„Š 1F ; 1F β†’ β„Š 0F }

π’¦β‚€βŠ«comm : 𝒦₀ ⊫ (xΒ·y β‰ˆΜ‡ yΒ·x)
π’¦β‚€βŠ«comm .⊫-proof 𝑩 inβ‚€ ρ = +-comm (ρ 0F) (ρ 1F)

V-commutative : 𝕍 ⊫ (xΒ·y β‰ˆΜ‡ yΒ·x)
V-commutative = V-id1 π’¦β‚€βŠ«comm

Birkhoff's theorem, specialized

Finally, the theorem itself and its converse, instantiated at 𝒦₀.

Birkhoff-β„• : {𝑨 : Algebra 0β„“ 0β„“}
  β†’ 𝑨 ∈ Mod (Th (V 0β„“ 1β„“ 𝒦₀)) β†’ 𝑨 ∈ V 0β„“ 1β„“ 𝒦₀
Birkhoff-β„• = Birkhoff {𝒦 = 𝒦₀}

Birkhoff-converse-β„• : {𝑨 : Algebra 0β„“ 0β„“}
  β†’ 𝑨 ∈ (V 0β„“ 1β„“ 𝒦₀) β†’ 𝑨 ∈ Mod (Th (V 0β„“ 1β„“ 𝒦₀))
Birkhoff-converse-β„• = Birkhoff-converse {𝒦 = 𝒦₀}

Birkhoff-β„•' : {𝑨 : Algebra 0β„“ 0β„“}
  β†’ 𝑨 ∈ Mod (Th 𝕍) β†’ 𝑨 ∈ V 0β„“ 1β„“ 𝒦₀
Birkhoff-β„•' = Birkhoff {𝒦 = 𝒦₀}

Birkhoff-converse-β„•' : {𝑨 : Algebra 0β„“ 0β„“}
  β†’ 𝑨 ∈ 𝕍 β†’ 𝑨 ∈ Mod (Th 𝕍)
Birkhoff-converse-β„•' = Birkhoff-converse {𝒦 = 𝒦₀}