---
layout: default
title : "Setoid.Congruences.Basic module (The Agda Universal Algebra Library)"
date : "2021-09-15"
author: "agda-algebras development team"
---

#### Congruences of Setoid Algebras

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

A **congruence** of an algebra `𝑨` is a binary relation on the carrier of `𝑨` that
is an equivalence relation, contains the setoid equality of `𝑨`, and is *compatible*
with the basic operations: applying an operation to argument tuples that are
related coordinatewise gives related results.

The compatibility half is `_βˆ£β‰ˆ_`{.AgdaFunction}; `IsCongruence`{.AgdaRecord} adds
the other two conditions, and `Con`{.AgdaFunction} is the bundled Ξ£-form that the
rest of the library passes around, with `IsCongruence→Con`{.AgdaFunction} and
`Con→IsCongruence`{.AgdaFunction} converting between them.

The reason to require containment of the setoid equality is that a congruence has
to be an equivalence relation on the *setoid*, not merely on the carrier: a
quotient by a relation that split an equality class would not be well defined.

With the congruence in hand `_β•±_`{.AgdaFunction} forms the quotient algebra, which
is the same carrier under the coarser equivalence, needing neither a quotient type
nor extensionality.  Kernels of homomorphisms are the primary source of congruences;
see [Setoid.Homomorphisms.Kernels][].


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

module Setoid.Congruences.Basic where

-- Imports from the Agda Standard Library ---------------------------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( _,_ ; Ξ£-syntax ; projβ‚‚ )
open import Data.Unit.Base   using ( ⊀ ; tt )
open import Function         using ( Func )
open import Level            using ( Level ; _βŠ”_ ; Lift ; lift ; lower )
open import Relation.Binary  using ( Setoid ; IsEquivalence )
                             renaming ( Rel to BinaryRel )

open import Relation.Binary.PropositionalEquality using ( refl )

-- Imports from the Agda Universal Algebras Library ------------------------------
open import Overture               using ( _|:_ ; Equivalence ; π“ž ; π“₯ ; Signature ; 𝑆 )
open import Setoid.Relations       using ( βŸͺ_⟫ ; _/_ ; βŸͺ_∼_⟫-elim )
open import Setoid.Algebras.Basic  using ( ov ; Algebra ; 𝔻[_] ; π•Œ[_] ; _^_ )

private variable Ξ± ρ β„“ : Level
```
-->

We now define the predicate `_βˆ£β‰ˆ_` so that, if `𝑨` denotes an algebra and `R` a
binary relation, then `𝑨 βˆ£β‰ˆ R` will represent the assertion that `R` is
*compatible* with all basic operations of `𝑨`. The formal definition is immediate
since all the work is done by the relation `|:`, which we defined above (see
[Setoid.Relations.Discrete][]).

```agda
-- Algebra compatibility with binary relation
_βˆ£β‰ˆ_ : (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) β†’ BinaryRel π•Œ[ 𝑨 ] β„“ β†’ Type _
𝑨 βˆ£β‰ˆ R = βˆ€ 𝑓 β†’ (𝑓 ^ 𝑨) |: R
```

A *congruence relation* of an algebra `𝑨` is defined to be an equivalence relation
that is compatible with the basic operations of `𝑨`.  This concept can be
represented in a number of alternative but equivalent ways. Formally, we define a
record type (`IsCongruence`) to represent the property of being a congruence, and
we define a Sigma type (`Con`) to represent the type of congruences of a given
algebra.

As mentioned above, congruences should contain the equality relation on the
underlying setoid.  That is, they must be *reflexive*; hence, the `reflexive`
field in the definition of `IsCongruence`.

```agda
module _ {𝑆 : Signature π“ž π“₯} (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) where
  open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ )
  record IsCongruence (ΞΈ : BinaryRel π•Œ[ 𝑨 ] β„“) : Type (π“ž βŠ” π“₯ βŠ” ρ βŠ” β„“ βŠ” Ξ±)  where
    constructor mkcon
    field
      reflexive : βˆ€ {aβ‚€ a₁} β†’ aβ‚€ β‰ˆ a₁ β†’ ΞΈ aβ‚€ a₁
      is-equivalence : IsEquivalence ΞΈ
      is-compatible  : 𝑨 βˆ£β‰ˆ ΞΈ

    Eqv : Equivalence π•Œ[ 𝑨 ] {β„“}
    Eqv = ΞΈ , is-equivalence

  open IsCongruence public

  Con : (β„“ : Level) β†’ Type (Ξ± βŠ” ρ βŠ” ov {𝑆 = 𝑆} β„“)
  Con β„“ = Ξ£[ ΞΈ ∈ BinaryRel π•Œ[ 𝑨 ] β„“ ] IsCongruence ΞΈ
```

Each of these types captures what it means to be a congruence and they are
equivalent in the sense that each implies the other. One implication is the
"uncurry" operation and the other is the second projection.

```agda
module _ {𝑆 : Signature π“ž π“₯} {𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ} where
  IsCongruenceβ†’Con : (ΞΈ : BinaryRel π•Œ[ 𝑨 ] β„“) β†’ IsCongruence 𝑨 ΞΈ β†’ Con 𝑨 β„“
  IsCongruence→Con θ p = θ , p

  Conβ†’IsCongruence : ((ΞΈ , _) : Con 𝑨 β„“) β†’ IsCongruence 𝑨 ΞΈ
  Con→IsCongruence (_ , p) = p
```

#### Quotient algebras

In many areas of abstract mathematics the *quotient* of an algebra `𝑨` with
respect to a congruence relation `ΞΈ` of `𝑨` plays an important role. This quotient
is typically denoted by `𝑨 / ΞΈ` and Agda allows us to define and express quotients
using this standard notation.

(Note that the forward-slash we use to denote the quotient is produced by typing
`\---` (in the Agda input method); it is a unicode character, and it is not the
ascii forward-slash that appears in the preceding paragraph.)

```agda
module _ {𝑆 : Signature π“ž π“₯}  where
  open Algebra  using ( Domain ; Interp )
  open Func     using ( cong ) renaming ( to to _⟨$⟩_ )

  _β•±_ : (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) β†’ Con 𝑨 β„“ β†’ Algebra Ξ± β„“
  (𝑨 β•± ΞΈ) .Domain = π•Œ[ 𝑨 ] / (Eqv (projβ‚‚ ΞΈ))
  (𝑨 β•± ΞΈ) .Interp ⟨$⟩ (f , a) = (f ^ 𝑨) a
  (𝑨 β•± ΞΈ) .Interp .cong {f , u} {.f , v} (refl , a) = is-compatible (projβ‚‚ ΞΈ) f a

  module _ (𝑨 : Algebra Ξ± ρ) where
    open Setoid 𝔻[ 𝑨 ] using ( _β‰ˆ_ )

    _/βˆ™_ : π•Œ[ 𝑨 ] β†’ (ΞΈ : Con 𝑨 β„“) β†’ π•Œ[ 𝑨 β•± ΞΈ ]
    a /βˆ™ ΞΈ = a

    /-≑ : ((_ΞΈ_ , ΞΈcon) : Con 𝑨 β„“){u v : π•Œ[ 𝑨 ]}
      β†’ βŸͺ u ⟫{Eqv ΞΈcon} β‰ˆ βŸͺ v ⟫{Eqv ΞΈcon} β†’ u ΞΈ v

    /-≑ ΞΈ uv = reflexive (Conβ†’IsCongruence ΞΈ) uv
```

#### The least and greatest congruences

Every algebra has a *least* and a *greatest* congruence.  The least is the
**diagonal** (identity) congruence `𝟘[ 𝑨 ]`, which relates exactly the
`β‰ˆ`-equal elements β€” it is the setoid equality, viewed as a congruence.  The
greatest is the **total** congruence `πŸ™[ 𝑨 ]`, which relates everything.  These
are the bottom and top of the congruence lattice (their order properties β€” that
they really are least and greatest β€” are recorded in
[Setoid.Congruences.Lattice][], where the containment order `_βŠ†_` is available).

Both are level-polymorphic via `Lift`, so they can be taken at whatever relation
level the surrounding context dictates (e.g. the absorbing level at which the
congruence lattice is assembled in [Setoid.Congruences.CompleteLattice][]); the
diagonal's result lives at `ρ βŠ” β„“`, the total's at `β„“`.

The only non-trivial obligation is **compatibility with the operations**.  For the
diagonal this is *exactly* the statement that the operations of `𝑨` respect its
setoid equality β€” i.e. the `cong` field of `Interp 𝑨` β€” which is why the diagonal
congruence cannot live in `Overture` (which has no algebra to appeal to) and
belongs here.  For the total congruence compatibility is trivial, since every two
elements are related.

```agda
  -- The least (diagonal) congruence of 𝑨: relates exactly the β‰ˆ-equal pairs.
  𝟘[_] : (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ){β„“ : Level} β†’ Con 𝑨 (ρ βŠ” β„“)
  𝟘[ 𝑨 ] {β„“} = (Ξ» x y β†’ Lift β„“ (x β‰ˆ y)) , mkcon (Ξ» e β†’ lift e) 𝟘-isEquiv 𝟘-compatible
    where
    open Setoid 𝔻[ 𝑨 ]  using ( _β‰ˆ_ )
                         renaming ( refl to β‰ˆrefl ; sym to β‰ˆsym ; trans to β‰ˆtrans )

    𝟘-isEquiv : IsEquivalence (Ξ» x y β†’ Lift β„“ (x β‰ˆ y))
    𝟘-isEquiv = record  { refl   = lift β‰ˆrefl
                        ; sym    = Ξ» p β†’ lift (β‰ˆsym (lower p))
                        ; trans  = Ξ» p q β†’ lift (β‰ˆtrans (lower p) (lower q)) }

    -- compatibility is precisely that the operations respect β‰ˆ (the cong of Interp)
    𝟘-compatible : 𝑨 βˆ£β‰ˆ Ξ» x y β†’ Lift β„“ (x β‰ˆ y)
    𝟘-compatible f h = lift (𝑨 .Interp .cong (refl , Ξ» i β†’ lower (h i)))

  -- The greatest (total) congruence of 𝑨: relates every pair.
  πŸ™[_] : (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ){β„“ : Level} β†’ Con 𝑨 β„“
  πŸ™[ 𝑨 ] {β„“} = (Ξ» _ _ β†’ Lift β„“ ⊀) , mkcon (Ξ» _ β†’ lift tt) πŸ™-isEquiv (Ξ» _ _ β†’ lift tt)
    where
    πŸ™-isEquiv : IsEquivalence (Ξ» (_ _ : π•Œ[ 𝑨 ]) β†’ Lift β„“ ⊀)
    πŸ™-isEquiv = record { refl = lift tt ; sym = Ξ» _ β†’ lift tt ; trans = Ξ» _ _ β†’ lift tt }
```