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

### The Congruence Generated by a Relation

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

The [Setoid.Congruences.Lattice][] module made `Con 𝑨` a meet-semilattice
under containment, with meet given by intersection (the tractable half of the
congruence lattice).  The join requires more work; it is the *least* congruence
containing the union; that is, the  **congruence generated by** the union.  This
module supplies the subsidiary result on which the join rests: for any binary
relation `R` on the carrier of `𝑨` there is a least congruence `Cg R` containing `R`.

We build `Cg R` as the inductively-defined closure `Gen R` of `R` under the
congruence-forming rules: it contains `R` (`base`), it contains the setoid equality
`_β‰ˆ_` (`rfl`), and it is closed under symmetry, transitivity, and the basic
operations (`symmetric`, `transitive`, `compatible`).  The following two facts make this *the*
generated congruence and constitute the **Congruence Generation Theorem**:

+  `Cg R` is a congruence containing `R` (so it is *an* upper bound of `R`); and
+  every congruence `ψ` containing `R` contains `Cg R` (so it is the *least* upper
   bound) β€” this is `Cg-least`, proved by induction on `Gen`.

From `Cg` we obtain the **join** `ΞΈ ∨ Ο† = Cg(ΞΈ βˆͺ Ο†)` and prove it is the least
upper bound of `ΞΈ` and `Ο†` in the containment order.  Because the closure quantifies
over the operations and the carrier, `Gen R` lands at level `π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ βŠ” β„“`
(not `β„“`); assembling this into a single-level `Lattice`/`CompleteLattice` bundle β€”
where that level is absorbed β€” is the remaining step of the congruence-lattice work
and is deferred to a follow-up.

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

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

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

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ---------------------------------------
open import Data.Product     using ( _,_ ; proj₁ ; projβ‚‚ )
open import Data.Sum.Base    using ( _⊎_ ; inj₁ ; injβ‚‚ ; [_,_] )
open import Level            using ( Level ; _βŠ”_ )
open import Relation.Binary  using ( Setoid ; IsEquivalence )
                             renaming ( Rel to BinaryRel ; _β‡’_ to _βŠ†_)
-- Imports from the Agda Universal Algebras Library ------------------------------
open import Overture                           using  ( OperationSymbolsOf ; ArityOf )
open import Setoid.Algebras.Basic     {𝑆 = 𝑆}  using  ( Algebra ; π•Œ[_] ; 𝔻[_] ; _^_ )
open import Setoid.Congruences.Basic  {𝑆 = 𝑆}  using  ( Con ; mkcon ; is-equivalence
                                                      ; is-compatible ; reflexive )
private variable Ξ± ρ β„“ β„“β€² : Level
```
-->

#### Inductive Generation of a Congruence

Fix an algebra `𝑨` and a binary relation `R` on its carrier.  `Gen R` is the
smallest relation containing `R` that is reflexive over `_β‰ˆ_`, symmetric,
transitive, and compatible with every basic operation.  The closure quantifies over
the operation symbols (`π“ž`), their arities (`π“₯`), and the carrier (`Ξ±`, `ρ`), so it
inhabits `BinaryRel π•Œ[ 𝑨 ] (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ βŠ” β„“)`; we name that level `π’ˆ β„“`.

```agda
module _ {𝑨 : Algebra Ξ± ρ} where
  open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ ) renaming ( refl to β‰ˆrefl )

  -- The level at which the generated congruence lives.
  π’ˆ : Level β†’ Level
  π’ˆ β„“ = π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ βŠ” β„“

  data Gen (R : BinaryRel π•Œ[ 𝑨 ] β„“) : BinaryRel π•Œ[ 𝑨 ] (π’ˆ β„“) where
    base : R βŠ† Gen R
    rfl         : {x y : π•Œ[ 𝑨 ]} β†’ x β‰ˆ y β†’ Gen R x y
    symmetric   : {x y : π•Œ[ 𝑨 ]} β†’ Gen R x y β†’ Gen R y x
    transitive  : {x y z : π•Œ[ 𝑨 ]} β†’ Gen R x y β†’ Gen R y z β†’ Gen R x z
    compatible  : (f : OperationSymbolsOf 𝑆) {u v : ArityOf 𝑆 f β†’ π•Œ[ 𝑨 ]}
      β†’ (βˆ€ i β†’ Gen R (u i) (v i)) β†’ Gen R ((f ^ 𝑨) u) ((f ^ 𝑨) v)

  Cg : (R : BinaryRel π•Œ[ 𝑨 ] β„“) β†’ Con 𝑨 (π’ˆ β„“)
  Cg R = Gen R , mkcon rfl g-isEquivalence compatible
    where
    open IsEquivalence using (refl ; sym ; trans )
    g-isEquivalence : IsEquivalence (Gen R)
    g-isEquivalence .refl  = rfl β‰ˆrefl
    g-isEquivalence .sym   = symmetric
    g-isEquivalence .trans = transitive
```

#### The Congruence Generation Theorem

`R` is contained in `Cg R` (the `base` constructor), and `Cg R` is the *least*
congruence with that property: any congruence `ψ` containing `R` already contains
`Gen R`.  The latter is proved by induction on the derivation of `Gen R x y`,
turning each closure rule into the corresponding congruence law of `ψ`.  Note `ψ` may
live at any relation level `β„“β€²`, so this is a genuinely heterogeneous statement.

```agda
  Cg-incl : (R : BinaryRel π•Œ[ 𝑨 ] β„“) β†’ R βŠ† Gen R
  Cg-incl R = base

  Cg-least : {R : BinaryRel π•Œ[ 𝑨 ] β„“} (ψ : Con 𝑨 β„“β€²) β†’ R βŠ† proj₁ ψ β†’ Gen R βŠ† proj₁ ψ
  Cg-least ψ RβŠ†Οˆ (base r) = RβŠ†Οˆ r
  Cg-least (_ , ψcon) RβŠ†Οˆ (rfl e) = reflexive ψcon e
  Cg-least ψ RβŠ†Οˆ (symmetric p) =
    IsEquivalence.sym (is-equivalence (ψ .projβ‚‚)) (Cg-least ψ RβŠ†Οˆ p)
  Cg-least ψ RβŠ†Οˆ (transitive p q) =
    IsEquivalence.trans (is-equivalence (projβ‚‚ ψ)) (Cg-least ψ RβŠ†Οˆ p) (Cg-least ψ RβŠ†Οˆ q)
  Cg-least ψ RβŠ†Οˆ (compatible f h) = is-compatible (projβ‚‚ ψ) f (Ξ» i β†’ Cg-least ψ RβŠ†Οˆ (h i))
```

Monotonicity follows immediately: if `R` is contained in `S` then `Cg R` is
contained in `Cg S` (take `ψ = Cg S`, which contains `S` hence `R`).

```agda
  Cg-mono : {R : BinaryRel π•Œ[ 𝑨 ] β„“} {S : BinaryRel π•Œ[ 𝑨 ] β„“β€²} β†’ R βŠ† S β†’ Gen R βŠ† Gen S
  Cg-mono {S = S} RβŠ†S = Cg-least (Cg S) (Ξ» r β†’ base (RβŠ†S r))
```

#### The Join of Two Congruences

For congruences `ΞΈ Ο† : Con 𝑨` the union `ΞΈ βˆͺ Ο†` of their underlying relations need
not be transitive, so we take the join to be the congruence it generates,
`ΞΈ ∨ Ο† = Cg(ΞΈ βˆͺ Ο†)`.  We record the order facts using a heterogeneous containment
`_βŠ‘_` (which coincides definitionally with the homogeneous `_≀_` of
[Setoid.Congruences.Lattice][] when the two levels agree), because the
join sits at the higher level `π’ˆ β„“`.

```agda
  -- Heterogeneous containment of congruences.
  _βŠ‘_ : Con 𝑨 β„“ β†’ Con 𝑨 β„“β€² β†’ Type (Ξ± βŠ” β„“ βŠ” β„“β€²)
  ΞΈ βŠ‘ Ο† = proj₁ ΞΈ βŠ† proj₁ Ο†
  infix 4 _βŠ‘_

  -- The union of the underlying relations of two congruences.
  _βˆͺα΅£_ : Con 𝑨 β„“ β†’ Con 𝑨 β„“ β†’ BinaryRel π•Œ[ 𝑨 ] β„“
  (ΞΈ βˆͺα΅£ Ο†) x y = proj₁ ΞΈ x y ⊎ proj₁ Ο† x y
  infixr 6 _βˆͺα΅£_

  _∨_ : Con 𝑨 β„“ β†’ Con 𝑨 β„“ β†’ Con 𝑨 (π’ˆ β„“)
  ΞΈ ∨ Ο† = Cg (ΞΈ βˆͺα΅£ Ο†)
  infixr 6 _∨_
```

The join is the least upper bound of its arguments: each argument is below it
(`base ∘ inj₁`, `base ∘ injβ‚‚`), and it is below any common upper bound (by
`Cg-least`, since the union is below any congruence above both arguments).

```agda
  ∨-upperΛ‘ : (ΞΈ Ο† : Con 𝑨 β„“) β†’ ΞΈ βŠ‘ (ΞΈ ∨ Ο†)
  ∨-upperΛ‘ _ _ p = base (inj₁ p)

  ∨-upperΚ³ : (ΞΈ Ο† : Con 𝑨 β„“) β†’ Ο† βŠ‘ (ΞΈ ∨ Ο†)
  ∨-upperΚ³ _ _ q = base (injβ‚‚ q)

  ∨-least : (ΞΈ Ο† : Con 𝑨 β„“) (ψ : Con 𝑨 β„“β€²) β†’ ΞΈ βŠ‘ ψ β†’ Ο† βŠ‘ ψ β†’ (ΞΈ ∨ Ο†) βŠ‘ ψ
  ∨-least _ _ ψ ΞΈβŠ‘Οˆ Ο†βŠ‘Οˆ = Cg-least ψ (Ξ» {x y} β†’ [ ΞΈβŠ‘Οˆ , Ο†βŠ‘Οˆ ])
```

#### The principal (single-pair) relation

For two carrier elements `a`, `b` of an algebra, `❴ a , b ❡`{.AgdaFunction} is the
relation that relates exactly `a` to `b`.  Its generated congruence `Cg ❴ a , b ❡` is
the *principal* congruence collapsing the one pair.

```agda
module principal (𝑨 : Algebra Ξ± ρ) where
  data ❴_,_❡ (a b : π•Œ[ 𝑨 ]) : BinaryRel π•Œ[ 𝑨 ] Ξ± where
    pᡣ : ❴ a , b ❡ a b
  open ❴_,_❡
```