---
layout: default
title : "Setoid.Congruences.Lattice module (The Agda Universal Algebra Library)"
date : "2026-06-01"
author: "agda-algebras development team"
---

#### The Congruence Lattice of a Setoid Algebra

This is the [Setoid.Congruences.Lattice][] module of the [Agda Universal Algebra Library][].

The congruences of an algebra `𝑨`, ordered by containment, form a complete lattice.
This module begins the formalization of that fact by promoting `Con 𝑨` to a
first-class ordered object: it defines the containment order `_βŠ†_`, the induced
equivalence `_≑_` of mutual containment, and the **meet** `ΞΈ ∧ Ο†`, which is the
relational intersection `ΞΈ ∩ Ο†`.  The intersection of two congruences is again a
congruence, and it is the greatest lower bound of the two arguments.  Thus we have a
partially ordered set which, with the meet operation, forms a semilattice.

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

open import Overture using (π“ž ; π“₯ ; Signature)

module Setoid.Congruences.Lattice {𝑆 : Signature π“ž π“₯} where

-- Imports from the Agda Standard Library ---------------------------------------
open import Agda.Primitive           using () renaming ( Set to Type )
open import Data.Product             using ( _Γ—_ ; _,_ ; proj₁ ; projβ‚‚ ; swap )
open import Data.Unit.Base           using ( tt )
open import Level                    using ( Level ; _βŠ”_ ; lift ; lower )
open import Relation.Binary          using ( Setoid ; IsEquivalence ; IsPartialOrder ; _β‡’_ )
                                     renaming ( Rel to BinaryRel )
open import Relation.Binary.Bundles  using ( Poset )
open import Relation.Binary.Lattice  using ( Infimum ; IsMeetSemilattice ; MeetSemilattice )

-- Imports from the Agda Universal Algebras Library ------------------------------
open import Setoid.Algebras.Basic     {𝑆 = 𝑆}  using  ( ov ; Algebra ; π•Œ[_] ; 𝔻[_] )
open import Setoid.Congruences.Basic  {𝑆 = 𝑆}  using  ( Con ; mkcon ; _βˆ£β‰ˆ_ ; reflexive
                                                      ; is-equivalence ; is-compatible
                                                      ; 𝟘[_] ; πŸ™[_] )
private variable Ξ± ρ β„“ : Level
```
-->

#### The containment order on congruences

For congruences `ΞΈ Ο† : Con 𝑨` we write `ΞΈ βŠ† Ο†` when the underlying relation of `ΞΈ`
is **contained** in that of `Ο†` ("contained" is with respect to subset inclusion on
`β„™(A Γ— A)`).  Classically this is the familiar (lattice) partial order on equivalence
relations, and it remains a partial order here β€” `_βŠ†_` is antisymmetric
**with respect to `_≑_`**, the equivalence of *mutual set containment*.  The only
subtlety is which equality counts as **equal congruences**.

The underlying relation of a congruence inhabits the `BinaryRel` type
(`BinaryRel A β„“ = A β†’ A β†’ Type β„“`), so mutual containment yields back-and-forth maps
between the proof-types `proj₁ ΞΈ x y` and `proj₁ Ο† x y` rather than a proof that the
packaged congruences are *propositionally* equal.

Upgrading `_≑_` to propositional equality would need function extensionality with
propositional extensionality/univalence (and proof-irrelevance for the `IsCongruence`
witness), and that's simply not available under   `--safe --cubical-compatible`; so we
take `_≑_` as the equality of congruences, exactly as the `Setoid/` discipline
dictates.  Classically `_≑_` collapses to propositional equality via propositional
extensionality.

```agda
module _ {𝑨 : Algebra Ξ± ρ} where
  -- ΞΈ βŠ† Ο† : the relation of ΞΈ is contained in the relation of Ο†.
  _βŠ†_ : Con 𝑨 β„“ β†’ Con 𝑨 β„“ β†’ Type (Ξ± βŠ” β„“)
  ΞΈ βŠ† Ο† = proj₁ ΞΈ β‡’ proj₁ Ο†
  infix 4 _βŠ†_

  -- ΞΈ ≑ Ο† : mutual containment (the equivalence the partial order is taken over).
  -- (the symbol ≑ is input as \doteqdot)
  _≑_ : Con 𝑨 β„“ β†’ Con 𝑨 β„“ β†’ Type (Ξ± βŠ” β„“)
  ΞΈ ≑ Ο† = ΞΈ βŠ† Ο† Γ— Ο† βŠ† ΞΈ
  infix 4 _≑_
```

The order is reflexive and transitive, and `_≑_` collapses it to a partial order.

```agda
  βŠ†-refl : {ΞΈ : Con 𝑨 β„“} β†’ ΞΈ βŠ† ΞΈ
  βŠ†-refl p = p

  βŠ†-trans : {ΞΈ Ο† ψ : Con 𝑨 β„“} β†’ ΞΈ βŠ† Ο† β†’ Ο† βŠ† ψ β†’ ΞΈ βŠ† ψ
  βŠ†-trans ΞΈβŠ†Ο† Ο†βŠ†Οˆ p = Ο†βŠ†Οˆ (ΞΈβŠ†Ο† p)

  -- A ≑-step entails a βŠ†-step (the `reflexive` field of a preorder).
  βŠ†-reflexive : {ΞΈ Ο† : Con 𝑨 β„“} β†’ ΞΈ ≑ Ο† β†’ ΞΈ βŠ† Ο†
  βŠ†-reflexive = proj₁

  -- Antisymmetry holds up to mutual containment, by definition of _≑_.
  βŠ†-antisym : {ΞΈ Ο† : Con 𝑨 β„“} β†’ ΞΈ βŠ† Ο† β†’ Ο† βŠ† ΞΈ β†’ ΞΈ ≑ Ο†
  βŠ†-antisym ΞΈβŠ†Ο† Ο†βŠ†ΞΈ = ΞΈβŠ†Ο† , Ο†βŠ†ΞΈ

  -- The components are written out directly rather than via βŠ†-refl/βŠ†-trans:
  -- because _βŠ†_ is a defined relation (not an injective type former), Agda
  -- cannot recover the implicit congruence arguments of those lemmas from the
  -- expected component types, so we inline the (trivial) proofs here.
  ≑-refl : {ΞΈ : Con 𝑨 β„“} β†’ ΞΈ ≑ ΞΈ
  ≑-refl = (Ξ» z β†’ z) , (Ξ» z β†’ z)

  ≑-sym : {ΞΈ Ο† : Con 𝑨 β„“} β†’ ΞΈ ≑ Ο† β†’ Ο† ≑ ΞΈ
  ≑-sym = swap

  ≑-trans : {ΞΈ Ο† ψ : Con 𝑨 β„“} β†’ ΞΈ ≑ Ο† β†’ Ο† ≑ ψ β†’ ΞΈ ≑ ψ
  ≑-trans (ΞΈβŠ†Ο† , Ο†βŠ†ΞΈ) (Ο†βŠ†Οˆ , ΟˆβŠ†Ο†) = (Ξ» p β†’ Ο†βŠ†Οˆ (ΞΈβŠ†Ο† p)) , (Ξ» p β†’ Ο†βŠ†ΞΈ (ΟˆβŠ†Ο† p))

  -- The implicit congruence (and level) arguments of the helper lemmas are bound
  -- by lambdas and forwarded explicitly: they cannot be inferred through the
  -- (non-injective) `Con 𝑨 β„“` carrier type at these function-typed fields.
  ≑-isEquivalence : IsEquivalence (_≑_ {β„“})
  ≑-isEquivalence {β„“} = record
    { refl = Ξ» {ΞΈ} β†’ ≑-refl {β„“} {ΞΈ}
    ; sym = Ξ» {ΞΈ} {Ο†} β†’ ≑-sym {β„“} {ΞΈ} {Ο†}
    ; trans = Ξ» {ΞΈ} {Ο†} {ψ} β†’ ≑-trans  {β„“} {ΞΈ} {Ο†} {ψ}
    }

  βŠ†-isPartialOrder : IsPartialOrder (_≑_ {β„“}) _βŠ†_
  βŠ†-isPartialOrder {β„“} = record
    { isPreorder = record  { isEquivalence = ≑-isEquivalence {β„“}
                           ; reflexive = Ξ» {ΞΈ} {Ο†} β†’ βŠ†-reflexive {β„“} {ΞΈ} {Ο†}
                           ; trans = Ξ» {ΞΈ} {Ο†} {ψ} β†’ βŠ†-trans {β„“} {ΞΈ} {Ο†} {ψ}
                           }
    ; antisym = Ξ» {ΞΈ} {Ο†} β†’ βŠ†-antisym {β„“} {ΞΈ} {Ο†}
    }
```

#### The bottom and top of the order

The diagonal congruence `𝟘[ 𝑨 ]` (defined in [Setoid.Congruences.Basic][]) is the
*least* congruence: it is contained in every congruence, because a congruence is
reflexive over `β‰ˆ` and `𝟘[ 𝑨 ]` relates only `β‰ˆ`-equal pairs.  The total congruence
`πŸ™[ 𝑨 ]` is the *greatest*: every congruence is contained in it, since it relates
everything.  These are the `βŠ₯` and `⊀` of the congruence lattice.

```agda
  -- 𝟘[ 𝑨 ] is the least congruence (the minimum of the containment order).
  𝟘-min : {β„“ : Level}(ΞΈ : Con 𝑨 (ρ βŠ” β„“)) β†’ 𝟘[ 𝑨 ] {β„“} βŠ† ΞΈ
  𝟘-min ΞΈ p = reflexive (projβ‚‚ ΞΈ) (lower p)

  -- πŸ™[ 𝑨 ] is the greatest congruence (the maximum of the containment order).
  πŸ™-max : {β„“ : Level}(ΞΈ : Con 𝑨 β„“) β†’ ΞΈ βŠ† πŸ™[ 𝑨 ] {β„“}
  πŸ™-max ΞΈ _ = lift tt
```

#### Meet: the intersection of two congruences

The intersection `ΞΈ ∩ Ο†` holds at `(x , y)` exactly when both `ΞΈ` and `Ο†` do.  It
is again a congruence: it contains the setoid equality (reflexivity), it is an
equivalence relation (componentwise), and it is compatible with every basic
operation (componentwise, using the compatibility of `ΞΈ` and of `Ο†`).  We define
the underlying relation first, then bundle the `IsCongruence` proof.

```agda
  -- The underlying relation of the meet: pointwise conjunction.
  meetRel : Con 𝑨 β„“ β†’ Con 𝑨 β„“ β†’ BinaryRel π•Œ[ 𝑨 ] β„“
  meetRel ΞΈ Ο† x y = proj₁ ΞΈ x y Γ— proj₁ Ο† x y

  _∧_ : Con 𝑨 β„“ β†’ Con 𝑨 β„“ β†’ Con 𝑨 β„“
  ΞΈ ∧ Ο† = meetRel ΞΈ Ο† , mkcon m-reflexive m-isEquivalence m-compatible
    where
    ΞΈc = projβ‚‚ ΞΈ
    Ο†c = projβ‚‚ Ο†
    ΞΈe = is-equivalence ΞΈc
    Ο†e = is-equivalence Ο†c

    open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ )
    -- The meet contains the setoid equality because ΞΈ and Ο† both do.
    m-reflexive : βˆ€ {aβ‚€ a₁} β†’ aβ‚€ β‰ˆ a₁ β†’ meetRel ΞΈ Ο† aβ‚€ a₁
    m-reflexive e = reflexive ΞΈc e , reflexive Ο†c e

    open IsEquivalence using (refl ; sym ; trans )
    -- The meet is an equivalence relation, proved componentwise.
    m-isEquivalence : IsEquivalence (meetRel ΞΈ Ο†)
    m-isEquivalence .refl = ΞΈe .refl , Ο†e .refl
    m-isEquivalence .sym = Ξ» (p , q) β†’ ΞΈe .sym p , Ο†e .sym q
    m-isEquivalence .trans = Ξ» (p , q) (pβ€² , qβ€²) β†’ ΞΈe .trans p pβ€² , Ο†e .trans q qβ€²

    -- The meet is compatible with every basic operation, componentwise.
    m-compatible : 𝑨 βˆ£β‰ˆ meetRel ΞΈ Ο†
    m-compatible 𝑓 uv = is-compatible ΞΈc 𝑓 (Ξ» i β†’ proj₁ (uv i))
                      , is-compatible Ο†c 𝑓 (Ξ» i β†’ projβ‚‚ (uv i))
  infixr 7 _∧_
```

The meet is the *greatest lower bound* of its two arguments: it is below each of
them, and it is above any common lower bound.  These three facts are exactly the
`Infimum` of `_βŠ†_` at `_∧_`.

```agda
  ∧-lowerΛ‘ : {ΞΈ Ο† : Con 𝑨 β„“} β†’ ΞΈ ∧ Ο† βŠ† ΞΈ
  ∧-lowerΛ‘ = proj₁

  ∧-lowerΚ³ : {ΞΈ Ο† : Con 𝑨 β„“} β†’ ΞΈ ∧ Ο† βŠ† Ο†
  ∧-lowerΚ³ = projβ‚‚

  ∧-greatest : {ΞΈ Ο† ψ : Con 𝑨 β„“} β†’ ψ βŠ† ΞΈ β†’ ψ βŠ† Ο† β†’ ψ βŠ† ΞΈ ∧ Ο†
  ∧-greatest ΟˆβŠ†ΞΈ ΟˆβŠ†Ο† p = ΟˆβŠ†ΞΈ p , ΟˆβŠ†Ο† p

  -- As above, the implicit congruence arguments of ∧-lowerˑ/ʳ and ∧-greatest
  -- are not inferable from the expected component types, so we inline them.
  ∧-infimum : Infimum (_βŠ†_ {β„“}) _∧_
  ∧-infimum ΞΈ Ο† = proj₁ , projβ‚‚ , Ξ» ψ ΟˆβŠ†ΞΈ ΟˆβŠ†Ο† p β†’ ΟˆβŠ†ΞΈ p , ΟˆβŠ†Ο† p

  open IsMeetSemilattice

  ∧-isMeetSemilattice : IsMeetSemilattice (_≑_ {β„“}) _βŠ†_ _∧_
  ∧-isMeetSemilattice .isPartialOrder = βŠ†-isPartialOrder
  ∧-isMeetSemilattice .infimum = ∧-infimum
```

#### The poset and meet-semilattice of congruences

Finally we assemble the standard-library bundles.  At a fixed relation level `β„“`,
`Con-Poset 𝑨` is the poset `(Con 𝑨, ≑, βŠ†)` and `Con-MeetSemilattice 𝑨` equips it
with the meet `_∧_`.  (The full lattice and complete lattice, with the join and
the bounds `βŠ₯`/`⊀`, are built in the subsequent steps of #271.)

```agda
module _ (𝑨 : Algebra Ξ± ρ) {β„“ : Level} where
  Con-Poset : Poset (Ξ± βŠ” ρ βŠ” ov β„“) (Ξ± βŠ” β„“) (Ξ± βŠ” β„“)
  Con-Poset = record  { Carrier = Con 𝑨 β„“ ; _β‰ˆ_ = _≑_ ; _≀_ = _βŠ†_
                      ; isPartialOrder  = βŠ†-isPartialOrder }

  Con-MeetSemilattice : MeetSemilattice (Ξ± βŠ” ρ βŠ” ov β„“) (Ξ± βŠ” β„“) (Ξ± βŠ” β„“)
  Con-MeetSemilattice = record  { Carrier = Con 𝑨 β„“
                                ; _β‰ˆ_ = _≑_
                                ; _≀_ = _βŠ†_
                                ; _∧_ = _∧_
                                ; isMeetSemilattice  = ∧-isMeetSemilattice
                                }
```