Skip to content

Setoid.Congruences.Generation

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.

{-# 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 π’ˆ β„“.

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.

  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).

  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 π’ˆ β„“.

  -- 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).

  ∨-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 ❡ is the relation that relates exactly a to b. Its generated congruence Cg ❴ a , b ❡ is the principal congruence collapsing the one pair.

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