Examples.Setoid.CongruenceLattice

Worked example: the congruence lattice of a two-element algebra

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

We exercise Setoid.Congruences.CompleteLattice on the smallest nontrivial example: the two-element algebra 𝟚 in the empty signature (no operations), whose carrier is Bool under propositional equality. Because there are no operations, every equivalence relation on Bool is automatically a congruence, so Con 𝟚 is just the lattice of equivalence relations on a two-element set — the two-element chain ⊥ < ⊤, where ⊥ is the diagonal (≡) and ⊤ is the all-relation.

We instantiate the Lattice, BoundedLattice, and CompleteLattice bundles for 𝟚, and verify the lattice is genuinely nontrivial by proving ⊤ ⋬ ⊥.

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

module Examples.Setoid.CongruenceLattice where

-- Imports from Agda and the Agda Standard Library ------------------------------
open import Data.Bool.Base    using ( Bool ; true ; false )
open import Data.Empty        using ( ⊥ )
open import Data.Product      using ( _,_ )
open import Function          using ( Func )
open import Level             using ( 0ℓ ; lift )
open import Relation.Binary   using ( Setoid )
open import Relation.Binary.PropositionalEquality as ≡ using ( _≡_ )
open import Relation.Nullary  using ( ¬_ )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Overture using ( Signature )

open Func renaming ( to to _⟨$⟩_ )

The empty signature and the two-element algebra 𝟚

The empty signature has no operation symbols (⊥), hence no arities.

𝑆₀ : Signature 0ℓ 0ℓ
𝑆₀ = ⊥ , λ ()

open import Setoid.Algebras {𝑆 = 𝑆₀}     using ( Algebra )
open import Setoid.Congruences {𝑆 = 𝑆₀}  using ( Con ; mkcon )
open import Setoid.Signatures            using ( ⟨_⟩ )

-- The two-element algebra: carrier Bool with ≡, and no operations to interpret.
𝟚 : Algebra 0ℓ 0ℓ
𝟚 = record { Domain = ≡.setoid Bool ; Interp = interp }
  where
  interp : Func (⟨ 𝑆₀ ⟩ (≡.setoid Bool)) (≡.setoid Bool)
  interp ⟨$⟩ (() , _)
  cong interp {() , _}

The Diagonal Congruence

Propositional equality _≡_ is a congruence of 𝟚: it is reflexive over the setoid equality (which is _≡_ here), an equivalence relation, and — since 𝑆₀ has no operations — compatibility is vacuous.

Δ : Con 𝟚 0ℓ
Δ = _≡_ , mkcon  (λ e → e)
                 (record { refl = ≡.refl ; sym = ≡.sym ; trans = ≡.trans })
                 (λ ())

Instantiating the bundles

With the base level ℓ₀ = 0ℓ the absorbing level L is 0ℓ, so the congruence lattice of 𝟚 is the chain on Con 𝟚 {0ℓ}. All three bundles type-check.

open import Setoid.Congruences.Lattice {𝑆 = 𝑆₀} using ( _⊆_ )
open import Setoid.Congruences.CompleteLattice {𝑆 = 𝑆₀}
  using ( Con-Lattice ; Con-BoundedLattice ; Con-CompleteLattice ; 1ᴬ ; 0ᴬ ; 0ᴬ-minimum )

Con𝟚-Lattice          = Con-Lattice         𝟚 0ℓ
Con𝟚-BoundedLattice   = Con-BoundedLattice  𝟚 0ℓ
Con𝟚-CompleteLattice  = Con-CompleteLattice 𝟚 0ℓ

Nontriviality: ⊤ ⋬ ⊥

The top and bottom congruences are distinct. If we had ⊤ ≤ ⊥, then composing with 0 ≤ Δ (the bottom is the least congruence, so it is below Δ) would give ⊤ ≤ Δ; but ⊤ relates true and false while Δ (namely _≡_) does not, so true ≡ false — a contradiction.

Con𝟚-nontrivial : ¬ ( (1ᴬ 𝟚 0ℓ) ⊆ (0ᴬ 𝟚 0ℓ) )
Con𝟚-nontrivial ⊤≤⊥ with 0ᴬ-minimum 𝟚 0ℓ Δ (⊤≤⊥ {true} {false} (lift _))
... | ()