---
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][].

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

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

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

-- Imports from the Agda Standard Library ---------------------------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( _,_ ; Ξ£-syntax ; proj₁ ; 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 )
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.

Congruences should obviously contain the equality relation on the underlying
setoid. That is, they must be reflexive. Unfortunately this doesn't come for free
(e.g., as part of the definition of `IsEquivalence` on Setoid), so we must add the
field `reflexive` to the definition of `IsCongruence`. (In fact, we should
probably redefine equivalence relation on setoids to be reflexive with respect to
the underlying setoid equality (and not just with respect to _≑_).)

```agda
module _ (𝑨 : 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
IsCongruenceβ†’Con : {𝑨 : Algebra Ξ± ρ}(ΞΈ : BinaryRel π•Œ[ 𝑨 ] β„“) β†’ IsCongruence 𝑨 ΞΈ β†’ Con 𝑨 β„“
IsCongruence→Con θ p = θ , p

Conβ†’IsCongruence : {𝑨 : Algebra Ξ± ρ}((ΞΈ , _) : 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.

```agda
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 𝑨 β„“){u v : π•Œ[ 𝑨 ]}
    β†’ βŸͺ u ⟫{Eqv (projβ‚‚ ΞΈ)} β‰ˆ βŸͺ v ⟫{Eqv (projβ‚‚ ΞΈ)} β†’ (proj₁ ΞΈ) 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 (cong (Interp 𝑨) (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 }
```