Agda UALib β

### Congruence Relations

This section presents the Algebras.Congruences module of the Agda Universal Algebra Library.

```
{-# OPTIONS --without-K --exact-split --safe #-}

open import Algebras.Signatures using (Signature; π; π₯)

module Algebras.Congruences {π : Signature π π₯} where

open import Algebras.Products {π = π} public

```

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.

```
module _ {π¦ π€ : Universe} where

record IsCongruence (π¨ : Algebra π€ π)(ΞΈ : Rel β£ π¨ β£ π¦) : ov π¦ β π€ Μ  where
constructor mkcon
field       is-equivalence : IsEquivalence ΞΈ
is-compatible  : compatible π¨ ΞΈ

Con : (π¨ : Algebra π€ π) β π€ β ov π¦ Μ
Con π¨ = Ξ£ ΞΈ κ ( Rel β£ π¨ β£ π¦ ) , 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.

```
IsCongruenceβCon : {π¨ : Algebra π€ π}(ΞΈ : Rel β£ π¨ β£ π¦) β IsCongruence π¨ ΞΈ β Con π¨
IsCongruenceβCon ΞΈ p = ΞΈ , p

ConβIsCongruence : {π¨ : Algebra π€ π} β ((ΞΈ , _) : Con π¨) β IsCongruence π¨ ΞΈ
ConβIsCongruence ΞΈ = β₯ ΞΈ β₯

```

#### Example

We defined the zero relation `π` in the Relations.Discrete module. We now build the trivial congruence, which has `π` as its underlying relation. Observe that `π` is equivalent to the identity relation `β‘` and these are obviously both equivalence relations. In fact, we already proved this of `β‘` in the Overture.Equality module, so we simply apply the corresponding proofs.

```
π-IsEquivalence : {A : π€ Μ} β  IsEquivalence {A = A} π
π-IsEquivalence = record {rfl = refl; sym = β‘-sym; trans = β‘-trans}

```

Next we formally record another obvious factβthat `π-rel` is compatible with all operations of all algebras.

```
π-compatible-op : funext π₯ π€ β {π¨ : Algebra π€ π} (π : β£ π β£) β (π Μ π¨) |: π
π-compatible-op fe {π¨} π {i}{j} ptws0  = ap (π Μ π¨) (fe ptws0)

π-compatible : funext π₯ π€ β {π¨ : Algebra π€ π} β compatible π¨ π
π-compatible fe {π¨} = Ξ» π args β π-compatible-op fe {π¨} π args

```

Finally, we have the ingredients need to construct the zero congruence of any algebra we like.

```
Ξ : (π¨ : Algebra π€ π){fe : funext π₯ π€} β IsCongruence π¨ π
Ξ π¨ {fe} = mkcon π-IsEquivalence (π-compatible fe)

π : (π¨ : Algebra π€ π){fe : funext π₯ π€} β Con{π€} π¨
π π¨ {fe} = IsCongruenceβCon π (Ξ π¨ {fe})

```

A concrete example is `βͺπβ«[ π¨ β± ΞΈ ]`, presented in the next subsection.

#### 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.1

```
module _ {π€ π¦ : Universe} where

_β±_ : (π¨ : Algebra π€ π) β Con{π¦} π¨ β Algebra (π€ β π¦ βΊ) π

π¨ β± ΞΈ = (β£ π¨ β£ / β£ ΞΈ β£)  ,                               -- the domain of the quotient algebra

Ξ» π π β βͺ (π Μ π¨)(Ξ» i β  fst β₯ π i β₯) β«           -- the basic operations of the quotient algebra

```

Example. If we adopt the notation `π[ π¨ β± ΞΈ ]` for the zero (or identity) relation on the quotient algebra `π¨ β± ΞΈ`, then we define the zero relation as follows.

```

π[_β±_] : (π¨ : Algebra π€ π)(ΞΈ : Con {π¦} π¨) β Rel (β£ π¨ β£ / β£ ΞΈ β£)(π€ β π¦ βΊ)
π[ π¨ β± ΞΈ ] = Ξ» u v β u β‘ v

```

From this we easily obtain the zero congruence of `π¨ β± ΞΈ` by applying the `Ξ` function defined above.

```
π[_β±_] : (π¨ : Algebra π€ π)(ΞΈ : Con{π¦} π¨){fe : funext π₯ (π€ β π¦ βΊ)} β Con (π¨ β± ΞΈ)
π[ π¨ β± ΞΈ ] {fe} = π[ π¨ β± ΞΈ ] , Ξ (π¨ β± ΞΈ) {fe}

```

Finally, the following elimination rule is sometimes useful.

```
module _ {π€ π¦ : Universe}{π¨ : Algebra π€ π} where
open IsCongruence

/-β‘ : (ΞΈ : Con{π¦} π¨){u v : β£ π¨ β£} β βͺ u β« {β£ ΞΈ β£} β‘ βͺ v β« β β£ ΞΈ β£ u v
/-β‘ ΞΈ refl = IsEquivalence.rfl (is-equivalence β₯ ΞΈ β₯)

```

1 Unicode Hints. Produce the `β±` symbol in agda2-mode by typing `\---` and then `C-f` a number of times.