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