↑ Top


Quotients

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 a b  : Level

Equivalence relations

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 a  {ρ : Level}  Type (a  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.

Kernels

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


open Level
ker-IsEquivalence : {A : Type a}{B : Type b}(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 a}{B : Type b}(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))
                                  }

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

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}  A  {ρ : Level}  BinRel A ρ  Pred A ρ
[ u ]{ρ} R = R u      -- (the R-block containing u : A)

-- Alternative notation
[_/_] : {A : Type a}  A  {ρ : Level}  Equivalence A {ρ}  Pred A ρ
[ u / R ] =  R  u

-- Alternative notation
Block : {A : Type a}  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 a}{ρ : Level}
                (P : Pred A ρ){R : BinRel A ρ} : Type(a  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 a){ρ : Level}  Equivalence A{ρ}  Type(a  suc ρ)
Quotient A R = Σ[ P  Pred A _ ] IsBlock P { R }

_/_ : (A : Type a){ρ : Level}  BinRel A ρ  Type(a  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.


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

Dually, the next type provides an elimination rule.


⌞_⌟ : {a : Level}{A : Type a}{ρ : 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 a}
          {ρ : 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 a) → {ρ : Level} → BinRel A (a ⊔ ρ)
0[ A ] {ρ} = λ x y → Lift ρ (x ≡ y)

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


0[_]IsEquivalence : (A : Type a){ρ : 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 a) {ρ : Level}  Equivalence A {a  ρ}
0[ A ]Equivalence {ρ} = 0[ A ] {ρ} , 0[ A ]IsEquivalence


⟪_∼_⟫-elim : {A : Type a}  (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 a}{ρ : Level}(Q R : Pred A ρ)  Q  R  Q  R
≡→⊆ Q .Q PE.refl {x} Qx = Qx

← Base.Relations.Properties Base.Equality →