---
layout: default
title : "Setoid.Congruences.CompleteLattice module (The Agda Universal Algebra Library)"
date : "2026-06-02"
author: "agda-algebras development team"
---
### The Complete Lattice of Congruences
This is the [Setoid.Congruences.CompleteLattice][] module of the [Agda Universal Algebra Library][].
[Setoid.Congruences.Lattice][] gave the meet (intersection) and the
containment order, and [Setoid.Congruences.Generation][] gave the join
`θ ∨ φ = Cg(θ ∪ φ)` via the congruence-generation theorem. This module assembles
those pieces into the **congruence lattice** of an algebra and shows it is
*complete*.
The one wrinkle is universe levels. The meet preserves the relation level `ℓ`, but
the join lands at `𝒈 ℓ = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ` (the closure quantifies over the
operations and the carrier). To make meet and join the *same* binary operation on a
*single* type, we evaluate the congruence lattice at a relation level that already
absorbs that bump: for a base level `ℓ₀`, at which `𝒈 L = L`,
L = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ₀.
At level `L` both `_∧_` and `_∨_` are operations on `Con 𝑨 {L}`, so they fit a
standard-library `Lattice` bundle, and with the bounds `⊥`/`⊤` a `BoundedLattice`.
For completeness we add infinitary meets `⨅` (intersection of a family) and joins
`⨆` (generated by the union of a family), each proved to be the relevant
greatest-lower / least-upper bound, and package them in the `CompleteLattice` record
of [Order.CompleteLattice][].
The family index `I` is required to live at the base level `ℓ₀`, so the lattice is
complete with respect to `ℓ₀`-small families — the usual predicative reading.
<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
open import Overture using (𝓞 ; 𝓥 ; Signature)
module Setoid.Congruences.CompleteLattice {𝑆 : Signature 𝓞 𝓥} where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Product using ( _,_ ; proj₁ ; proj₂ ; Σ-syntax )
open import Level using ( Level ; _⊔_ )
open import Relation.Binary using ( Setoid ; IsEquivalence )
open import Relation.Binary.Definitions using ( Maximum ; Minimum )
open import Relation.Binary.Lattice using ( Supremum ; IsLattice
; Lattice ; IsBoundedLattice
; BoundedLattice )
open import Setoid.Algebras.Basic {𝑆 = 𝑆} using ( ov ; Algebra ; 𝕌[_] ; 𝔻[_] )
open import Order.CompleteLattice using ( CompleteLattice )
open import Setoid.Congruences.Basic {𝑆 = 𝑆} using ( Con ; mkcon ; _∣≈_
; reflexive ; is-equivalence
; is-compatible ; 𝟘[_] ; 𝟙[_] )
open import Setoid.Congruences.Lattice {𝑆 = 𝑆} using ( _≑_ ; _⊆_ ; _∧_
; ⊆-isPartialOrder
; ∧-infimum ; 𝟘-min ; 𝟙-max )
open import Setoid.Congruences.Generation {𝑆 = 𝑆} using ( Cg ; Cg-least ; base
; _∨_ ; ∨-upperˡ
; ∨-upperʳ ; ∨-least )
private variable α ρ ℓ₀ : Level
```
-->
#### The congruence lattice at the absorbing level `L`
We fix an algebra `𝑨` and a base level `ℓ₀`, and work with congruences whose
relation level is `L = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ₀`. Because level join is idempotent,
`𝒈 L = L`, so the join `_∨_` (whose codomain is `Con 𝑨 {𝒈 L}`) is an operation on
`Con 𝑨 {L}`, exactly like the meet.
```agda
module _ (𝑨 : Algebra α ρ) (ℓ₀ : Level) where
L : Level
L = 𝓞 ⊔ 𝓥 ⊔ α ⊔ ρ ⊔ ℓ₀
private
Conᴸ : Type (α ⊔ ρ ⊔ ov L)
Conᴸ = Con 𝑨 L
```
The join is the least upper bound: the two upper-bound facts come from `Generation`,
and the universality is `∨-least`.
```agda
Con-supremum : Supremum (_⊆_ {𝑨 = 𝑨} {L}) _∨_
Con-supremum θ φ = ∨-upperˡ θ φ
, ∨-upperʳ θ φ
, λ ψ θ⊆ψ φ⊆ψ → ∨-least θ φ ψ θ⊆ψ φ⊆ψ
```
Assembling the partial order, the supremum, and the meet's infimum gives the lattice.
```agda
Con-isLattice : IsLattice (_≑_ {𝑨 = 𝑨} {L}) _⊆_ _∨_ _∧_
Con-isLattice = record { isPartialOrder = ⊆-isPartialOrder
; supremum = Con-supremum
; infimum = ∧-infimum
}
Con-Lattice : Lattice (α ⊔ ρ ⊔ ov L) (α ⊔ L) (α ⊔ L)
Con-Lattice = record { Carrier = Conᴸ
; _≈_ = _≑_
; _≤_ = _⊆_
; _∨_ = _∨_
; _∧_ = _∧_
; isLattice = Con-isLattice
}
```
#### The bounds: zero and total congruences
The bottom congruence `0ᴬ` is the **diagonal** congruence `𝟘[ 𝑨 ]` and the top
congruence `1ᴬ` is the **total** congruence `𝟙[ 𝑨 ]`, both from
[Setoid.Congruences.Basic][], taken at the absorbing level `L`. Their minimality
and maximality are the order facts `𝟘-min` / `𝟙-max` of
[Setoid.Congruences.Lattice][].
(The least congruence is the diagonal — the identity relation viewed as a
congruence — not the empty relation: the empty relation is not even reflexive, so
it is not a congruence at all. An earlier version defined `0ᴬ = Cg 0A` as the
congruence *generated by* the empty relation; that is in fact the diagonal, since
`Cg` closes under reflexivity over `≈`, but the direct definition `𝟘[ 𝑨 ]` is the
standard and clearer one.)
```agda
0ᴬ : Conᴸ
0ᴬ = 𝟘[ 𝑨 ] {L}
1ᴬ : Conᴸ
1ᴬ = 𝟙[ 𝑨 ] {L}
0ᴬ-minimum : Minimum _⊆_ 0ᴬ
0ᴬ-minimum θ = 𝟘-min {ℓ = L} θ
1ᴬ-maximum : Maximum _⊆_ 1ᴬ
1ᴬ-maximum θ = 𝟙-max θ
```
With the bounds the lattice becomes a bounded lattice (`1ᴬ` is the maximum, `0ᴬ` the
minimum).
```agda
Con-isBoundedLattice : IsBoundedLattice (_≑_ {𝑨 = 𝑨} {L}) _⊆_ _∨_ _∧_ 1ᴬ 0ᴬ
Con-isBoundedLattice = record { isLattice = Con-isLattice
; maximum = 1ᴬ-maximum
; minimum = 0ᴬ-minimum
}
Con-BoundedLattice : BoundedLattice (α ⊔ ρ ⊔ ov L) (α ⊔ L) (α ⊔ L)
Con-BoundedLattice = record { Carrier = Conᴸ
; _≈_ = _≑_
; _≤_ = _⊆_
; _∨_ = _∨_
; _∧_ = _∧_
; ⊤ = 1ᴬ
; ⊥ = 0ᴬ
; isBoundedLattice = Con-isBoundedLattice
}
```
#### Infinitary meets and joins
For a family `f : I → Con 𝑨 {L}` indexed by `I : Type ℓ₀`, the infinitary meet is the
intersection `⋀ f` (which holds at `(x , y)` iff every `f i` does), and the
infinitary join is the congruence generated by the union, `⋁ f = Cg(⋃ f)`. Both stay
at level `L` because `I` is `ℓ₀`-small. The meet is the greatest lower bound and the
join the least upper bound of the family.
```agda
module _ {I : Type ℓ₀} (f : I → Conᴸ) where
⋀ : Conᴸ
⋀ = (λ x y → (i : I) → proj₁ (f i) x y) , mkcon m-refl m-equiv m-comp
where
open Setoid 𝔻[ 𝑨 ] using ( _≈_ )
m-refl : ∀ {a₀ a₁} → a₀ ≈ a₁ → (i : I) → proj₁ (f i) a₀ a₁
m-refl e i = reflexive (proj₂ (f i)) e
m-equiv : IsEquivalence (λ x y → (i : I) → proj₁ (f i) x y)
m-equiv = record
{ refl = λ i → IsEquivalence.refl (is-equivalence (proj₂ (f i)))
; sym = λ p i → IsEquivalence.sym (is-equivalence (proj₂ (f i))) (p i)
; trans = λ p q i → IsEquivalence.trans (is-equivalence (proj₂ (f i))) (p i) (q i)
}
m-comp : 𝑨 ∣≈ (λ x y → (i : I) → proj₁ (f i) x y)
m-comp g h i = is-compatible (proj₂ (f i)) g (λ k → h k i)
⋁ : Conᴸ
⋁ = Cg (λ x y → Σ[ i ∈ I ] proj₁ (f i) x y)
⋀-lower : (i : I) → ⋀ ⊆ f i
⋀-lower i p = p i
⋀-greatest : (ψ : Conᴸ) → (∀ i → ψ ⊆ f i) → ψ ⊆ ⋀
⋀-greatest ψ ψ⊆f p i = ψ⊆f i p
⋁-upper : (i : I) → f i ⊆ ⋁
⋁-upper i p = base (i , p)
⋁-least : (ψ : Conᴸ) → (∀ i → f i ⊆ ψ) → ⋁ ⊆ ψ
⋁-least ψ f⊆ψ = Cg-least {𝑨 = 𝑨} ψ (λ (i , p) → f⊆ψ i p)
```
#### The complete lattice
Packaging the order with the infinitary operations and their universal properties
yields the complete lattice of congruences.
```agda
Con-CompleteLattice : CompleteLattice (α ⊔ ρ ⊔ ov L) (α ⊔ L) (α ⊔ L) ℓ₀
Con-CompleteLattice = record
{ Carrier = Conᴸ
; _≈_ = _≑_
; _≤_ = _⊆_
; isPartialOrder = ⊆-isPartialOrder
; ⨆ = ⋁
; ⨅ = ⋀
; ⨆-upper = λ f i → ⋁-upper f i
; ⨆-least = λ f x h → ⋁-least f x h
; ⨅-lower = λ f i → ⋀-lower f i
; ⨅-greatest = λ f x h → ⋀-greatest f x h
}
```