---
layout: default
file: "src/Examples/Setoid/HSPCommutativeMonoid.lagda.md"
title: "Examples.Setoid.HSPCommutativeMonoid module"
date: "2026-05-31"
author: "the agda-algebras development team"
---

### Worked example: Birkhoff's HSP theorem specialized to `(β„•, +, 0)` {#examples-setoid-hsp-commutativemonoid}

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
`𝒦`{.AgdaBound} of algebras over an arbitrary signature.  This module instantiates
that theorem at the singleton class `𝒦₀ = { (β„•, +, 0) }` over the
monoid signature `Sig-Monoid`{.AgdaFunction}, 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`{.AgdaFunction}, from identity preservation);
+  Birkhoff's theorem, specialized: every model of the equational theory of
   `V 𝒦₀` lies in `V 𝒦₀` (`Birkhoff-β„•`{.AgdaFunction});
+  and its converse (`Birkhoff-converse-β„•`{.AgdaFunction}).

<!--
```agda
{-# 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 )
```
-->

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

#### The generating algebra and the singleton class {#generating-algebra}

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

```agda
𝑨₀ : 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β€²`{.AgdaFunction} β€” the common-case
specialization of `V`{.AgdaFunction} that collapses its eight level parameters to
those of the generating class β€” giving a single concrete predicate
`𝕍`{.AgdaFunction} that the corollaries below can refer to without pinning any
level by hand or leaving unsolved level metavariables.

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

#### Corollary 1: the generator lies in its own variety {#in-its-variety}

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

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

#### Corollary 2: the variety is commutative {#variety-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.

```agda
-- 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 {#birkhoff-specialized}

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

```agda
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 {𝒦 = 𝒦₀}
```