This is the Base.Relations.Quotients module of the Agda Universal Algebra Library.

{-# OPTIONS --without-K --exact-split --safe #-} module Base.Relations.Quotients where -- Imports from Agda and the Agda Standard Library ---------------------------------------------- open import Agda.Primitive using () renaming ( Set to Type ) open import Data.Product using ( _,_ ; _×_ ; Σ-syntax ) renaming ( proj₁ to fst ; proj₂ to snd ) open import Level using ( Level ; _⊔_ ; suc ) open import Relation.Binary using ( IsEquivalence ; IsPartialEquivalence) renaming ( Rel to BinRel ) open import Relation.Unary using ( Pred ; _⊆_ ) open import Relation.Binary.PropositionalEquality as PE using ( _≡_ ) -- Imports from agda-algebras --------------------------------------------------------------------- open import Overture using ( ∣_∣ ) open import Base.Relations.Discrete using ( ker ; 0[_] ; kerlift ) open import Base.Relations.Properties using ( Reflexive ; Symmetric ; Transitive ) private variable α β χ : Level

A binary relation is called a *preorder* if it is reflexive and transitive.
An *equivalence relation* is a symmetric preorder. The property of being
an equivalence relation is represented in the Agda Standard Library by
a record type called `IsEquivalence`

. Here we define the `Equivalence`

type
which is inhabited by pairs `(r , p)`

where `r`

is a binary relation and `p`

is a proof that `r`

satisfies `IsEquivalence`

.

Equivalence : Type α → {ρ : Level} → Type (α ⊔ suc ρ) Equivalence A {ρ} = Σ[ r ∈ BinRel A ρ ] IsEquivalence r

Another way to represent binary relations is as the inhabitants of the
type `Pred(X × X) _`

, and we here define the `IsPartialEquivPred`

and `IsEquivPred`

types corresponding to such a representation.

module _ {X : Type χ}{ρ : Level} where record IsPartialEquivPred (R : Pred (X × X) ρ) : Type (χ ⊔ ρ) where field sym : Symmetric R trans : Transitive R record IsEquivPred (R : Pred (X × X) ρ) : Type (χ ⊔ ρ) where field refl : Reflexive R sym : Symmetric R trans : Transitive R reflexive : ∀ x y → x ≡ y → R (x , y) reflexive x .x PE.refl = refl

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.

open Level ker-IsEquivalence : {A : Type α}{B : Type β}(f : A → B) → IsEquivalence (ker f) ker-IsEquivalence f = record { refl = PE.refl ; sym = λ x → PE.sym x ; trans = λ x y → PE.trans x y } kerlift-IsEquivalence : {A : Type α}{B : Type β}(f : A → B){ρ : Level} → IsEquivalence (kerlift f ρ) kerlift-IsEquivalence f = record { refl = lift PE.refl ; sym = λ x → lift (PE.sym (lower x)) ; trans = λ x y → lift (PE.trans (lower x) (lower y)) }

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}`

.

Before defining the quotient type, we define a type representing inhabitants of quotients; i.e., blocks of a partition (recall partitions correspond to equivalence relations) -}

[_] : {A : Type α} → A → {ρ : Level} → BinRel A ρ → Pred A ρ [ u ]{ρ} R = R u -- (the R-block containing u : A) -- Alternative notation [_/_] : {A : Type α} → A → {ρ : Level} → Equivalence A {ρ} → Pred A ρ [ u / R ] = ∣ R ∣ u -- Alternative notation Block : {A : Type α} → A → {ρ : Level} → Equivalence A{ρ} → Pred A ρ Block 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.

record IsBlock {A : Type α}{ρ : Level} (P : Pred A ρ){R : BinRel A ρ} : Type(α ⊔ suc ρ) where constructor mkblk field blk : A P≡[blk] : P ≡ [ blk ]{ρ} 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.

Quotient : (A : Type α){ρ : Level} → Equivalence A{ρ} → Type(α ⊔ suc ρ) Quotient A R = Σ[ P ∈ Pred A _ ] IsBlock P {∣ R ∣} _/_ : (A : Type α){ρ : Level} → BinRel A ρ → Type(α ⊔ suc ρ) A / R = Σ[ P ∈ Pred A _ ] IsBlock P {R} infix -1 _/_

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

⟪_⟫ : {α : Level}{A : Type α}{ρ : Level} → A → {R : BinRel A ρ} → A / R ⟪ a ⟫{R} = [ a ] R , mkblk a PE.refl

Dually, the next type provides an *elimination rule*.

⌞_⌟ : {α : Level}{A : Type α}{ρ : Level}{R : BinRel A ρ} → A / R → A ⌞ _ , mkblk a _ ⌟ = a

Here `C`

is a predicate and `p`

is a proof of `C ≡ [ a ] R`

.

module _ {A : Type α} {ρ : Level} -- note: ρ is an implicit parameter {R : Equivalence A {ρ}} where open IsEquivalence []-⊆ : (x y : A) → ∣ R ∣ x y → [ x ]{ρ} ∣ R ∣ ⊆ [ y ] ∣ R ∣ []-⊆ x y Rxy {z} Rxz = IsEquivalence.trans (snd R) (IsEquivalence.sym (snd R) Rxy) Rxz []-⊇ : (x y : A) → ∣ R ∣ x y → [ y ] ∣ R ∣ ⊆ [ x ] ∣ R ∣ []-⊇ x y Rxy {z} Ryz = IsEquivalence.trans (snd R) Rxy Ryz ⊆-[] : (x y : A) → [ x ] ∣ R ∣ ⊆ [ y ] ∣ R ∣ → ∣ R ∣ x y ⊆-[] x y xy = IsEquivalence.sym (snd R) (xy (IsEquivalence.refl (snd R))) ⊇-[] : (x y : A) → [ y ] ∣ R ∣ ⊆ [ x ] ∣ R ∣ → ∣ R ∣ x y ⊇-[] x y yx = yx (IsEquivalence.refl (snd R))

An example application of these is the `block-ext`

type in the [Base.Relations.Extensionality] module.

Recall, from Base.Relations.Discrete, the zero (or “identity”) relation is

```
0[_] : (A : Type α) → {ρ : Level} → BinRel A (α ⊔ ρ)
0[ A ] {ρ} = λ x y → Lift ρ (x ≡ y)
```

This is obviously an equivalence relation, as we now confirm.

0[_]IsEquivalence : (A : Type α){ρ : Level} → IsEquivalence (0[ A ] {ρ}) 0[ A ]IsEquivalence {ρ} = record { refl = lift PE.refl ; sym = λ p → lift (PE.sym (lower p)) ; trans = λ p q → lift (PE.trans (lower p) (lower q)) } 0[_]Equivalence : (A : Type α) {ρ : Level} → Equivalence A {α ⊔ ρ} 0[ A ]Equivalence {ρ} = 0[ A ] {ρ} , 0[ A ]IsEquivalence ⟪_∼_⟫-elim : {A : Type α} → (u v : A) → {ρ : Level}{R : Equivalence A{ρ} } → ⟪ u ⟫{∣ R ∣} ≡ ⟪ v ⟫ → ∣ R ∣ u v ⟪ u ∼ .u ⟫-elim {ρ} {R} PE.refl = IsEquivalence.refl (snd R) ≡→⊆ : {A : Type α}{ρ : Level}(Q R : Pred A ρ) → Q ≡ R → Q ⊆ R ≡→⊆ Q .Q PE.refl {x} Qx = Qx