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

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 }

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.

^{1}**Unicode Hints** (agda2-mode). `\cl ↝ ⌞`

; `\clr ↝ ⌟`

.