Agda UALib ↑

### Equivalence Relations and Quotients

This section presents the Relations.Quotients module of the Agda Universal Algebra Library.

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

module Relations.Quotients where

open import Relations.Continuous public

```

#### Equivalence relations

Let `𝓤 : Universe` be a universe and `A : 𝓤 ̇` a type. In Relations.Discrete we defined a type representing a binary relation on A. In this module we will define types for binary relations that have special properties. The most important special properties of relations are the ones we now define.

```
module _ {𝓤 𝓦 : Universe} where

Refl : {A : 𝓤 ̇} → Rel A 𝓦 → 𝓤 ⊔ 𝓦 ̇
Refl _≈_ = ∀{x} → x ≈ x

Symm : {A : 𝓤 ̇} → Rel A 𝓦 → 𝓤 ⊔ 𝓦 ̇
Symm _≈_ = ∀{x}{y} → x ≈ y → y ≈ x

Antisymm : {A : 𝓤 ̇} → Rel A 𝓦 → 𝓤 ⊔ 𝓦 ̇
Antisymm _≈_ = ∀{x}{y} → x ≈ y → y ≈ x → x ≡ y

Trans : {A : 𝓤 ̇} → Rel A 𝓦 → 𝓤 ⊔ 𝓦 ̇
Trans _≈_ = ∀{x}{y}{z} → x ≈ y → y ≈ z → x ≈ z

```

The Type Topology library defines the following uniqueness-of-proofs principle for binary relations.

```
module hide-is-subsingleton-valued where

is-subsingleton-valued : {A : 𝓤 ̇} → Rel A 𝓦 → 𝓤 ⊔ 𝓦 ̇
is-subsingleton-valued  _≈_ = ∀ x y → is-subsingleton (x ≈ y)

open import MGS-Quotient using (is-subsingleton-valued) public

```

Thus, if `R : Rel A 𝓦`, then `is-subsingleton-valued R` is the assertion that for each pair `x y : A` there can be at most one proof that `R x y` holds.

In the Relations.Truncation module we introduce a number of similar but more general types used in the Agda UALib to represent uniqueness-of-proofs principles for relations of arbitrary arity over arbitrary types.

A binary relation is called a preorder if it is reflexive and transitive. An equivalence relation is a symmetric preorder. We define the property of being an equivalence relation as the following record type.

```
module _ {𝓤 𝓦 : Universe} where

record IsEquivalence {A : 𝓤 ̇}(R : Rel A 𝓦) : 𝓤 ⊔ 𝓦 ̇ where
field rfl : Refl R ; sym : Symm R ; trans : Trans R

```

And we define the type of equivalence relations over a given type `A` as follows.

```
Equivalence : 𝓤 ̇ → 𝓤 ⊔ 𝓦 ⁺ ̇
Equivalence A = Σ R ꞉ Rel A 𝓦 , IsEquivalence R

```

Thus, if we have `(R , p) : Equivalence A`, then `R` denotes a binary relation over `A` and `p` is of record type `IsEquivalence R` with fields containing the three proofs showing that `R` is an equivalence relation.

A prominent example of an equivalence relation is the kernel of any function.

```
ker-IsEquivalence : {A : 𝓤 ̇}{B : 𝓦 ̇}(f : A → B) → IsEquivalence (ker f)
ker-IsEquivalence f = record { rfl = refl; sym = λ z → ≡-sym z ; trans = λ p q → ≡-trans p q }

```

#### Equivalence classes (blocks)

If `R` is an equivalence relation on `A`, then for each `u : A` there is an equivalence class (or equivalence block, or `R`-block) containing `u`, which we denote and define by `[ u ] := {v : A | R u v}`.

```
[_] : {A : 𝓤 ̇} → A → {R : Rel A 𝓦} → Pred A 𝓦
[ u ]{R} = R u

infix 60 [_]

```

Thus, `v ∈ [ u ]` if and only if `R u v`, as desired. We often refer to `[ u ]` as the `R`-block containing `u`.

A predicate `C` over `A` is an `R`-block if and only if `C ≡ [ u ]` for some `u : A`. We represent this characterization of an `R`-block as follows.

```
module _ {𝓤 𝓦 : Universe} where

IsBlock : {A : 𝓤 ̇}(C : Pred A 𝓦){R : Rel A 𝓦} → 𝓤 ⊔ 𝓦 ⁺ ̇
IsBlock {A} C {R} = Σ u ꞉ A , C ≡ [ u ] {R}

```

Thus, a proof of `IsBlock C` is a pair `(u , p)`, with `u : A` and `p` is a proof of `C ≡ [ u ] {R}`.

If `R` is an equivalence relation on `A`, then the quotient of `A` modulo `R` is denoted by `A / R` and is defined to be the collection `{[ u ] ∣ y : A}` of all `R`-blocks.1

```
_/_ : (A : 𝓤 ̇ ) → Rel A 𝓦 → 𝓤 ⊔ (𝓦 ⁺) ̇
A / R = Σ C ꞉ Pred A 𝓦 , IsBlock C {R}

infix -1 _/_

```

We use the following type to represent an \ab R-block with a designated representative.

```
⟪_⟫ : {A : 𝓤 ̇} → A → {R : Rel A 𝓦} → A / R
⟪ a ⟫{R} = [ a ]{R} , (a  , refl)

```

Dually, the next type provides an elimination rule.2

```
⌞_⌟ : {A : 𝓤 ̇}{R : Rel A 𝓦} → A / R  → A
⌞ C , a , p ⌟ = a

```

Here `C` is a predicate and `p` is a proof of `C ≡ [ a ] R`.

It will be convenient to have the following subset inclusion lemmas on hand when working with quotient types.

```
module _ {𝓤 𝓦 : Universe}{A : 𝓤 ̇}{x y : A}{R : Rel A 𝓦} where

open IsEquivalence
/-subset : IsEquivalence R → R x y →  [ x ]{R} ⊆  [ y ]{R}
/-subset Req Rxy {z} Rxz = (trans Req) ((sym Req) Rxy) Rxz

/-supset : IsEquivalence R → R x y →  [ y ]{R} ⊆ [ x ]{R}
/-supset Req Rxy {z} Ryz = (trans Req) Rxy Ryz

```

An example application of these is the `block-ext` type in the Relations.Extensionality module.

1Unicode Hints (agda2-mode). `\cl ↝ ⌞`; `\clr ↝ ⌟`.