Skip to content

Setoid.Relations.Quotients

Quotients of setoids

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

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.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 ( _Γ—_ to _∧_ )
open import Function          using ( id ) renaming ( Func to _⟢_ )
open import Level using ( Level ; _βŠ”_ ; suc )
open import Relation.Binary   using ( IsEquivalence ) renaming ( Rel to BinaryRel )
open import Relation.Unary    using ( Pred ; _∈_ ; _βŠ†_ )
open import Relation.Binary   using ( Setoid )
open import Relation.Binary.PropositionalEquality as ≑
                              using ( _≑_ )

-- Imports from agda-algebras -----------------------------------------------------
open import Overture                   using ( proj₁ ; projβ‚‚ ; [_] ; Equivalence )
open import Setoid.Relations.Discrete  using ( fker )

private variable Ξ± Ξ² ρᡃ ρᡇ β„“ : Level

Kernels

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

open _⟢_ using ( cong )

module _ {𝐴 : Setoid Ξ± ρᡃ}{𝐡 : Setoid Ξ² ρᡇ} where
  open Setoid 𝐴  using ( refl ) renaming (Carrier to A )
  open Setoid 𝐡  using ( sym ; trans )

  ker-IsEquivalence : (f : 𝐴 ⟢ 𝐡) β†’ IsEquivalence (fker f)
  IsEquivalence.refl   (ker-IsEquivalence f) = cong f refl
  IsEquivalence.sym    (ker-IsEquivalence f) = sym
  IsEquivalence.trans  (ker-IsEquivalence f) = trans

record IsBlock  {A : Type α}{ρ : Level}
                (P : Pred A ρ){R : BinaryRel A ρ} : Type(Ξ± βŠ” suc ρ) where
  constructor mkblk
  field
    a : A
    Pβ‰ˆ[a] : βˆ€ x β†’ (x ∈ P β†’ [ a ]{ρ} R x) ∧ ([ a ]{ρ} R x β†’ x ∈ P)

open IsBlock

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 Ξ±) β†’ Equivalence A{β„“} β†’ Type(Ξ± βŠ” suc β„“)
Quotient A R = Ξ£[ P ∈ Pred A _ ] IsBlock P {(proj₁ R)}

_/_ : (A : Type Ξ±) β†’ Equivalence A{β„“} β†’ Setoid _ _
A / R = record { Carrier = A ; _β‰ˆ_ = (proj₁ R) ; isEquivalence = (projβ‚‚ R) }

infix -1 _/_

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

open Setoid
βŸͺ_⟫ : {Ξ± : Level}{A : Type Ξ±} β†’ A β†’ {R : Equivalence A{β„“}} β†’ Carrier (A / R)
βŸͺ a ⟫{R} = a

module _ {A : Type Ξ±}{R : Equivalence A{β„“} } where

  open Setoid (A / R) using () renaming ( _β‰ˆ_ to _β‰ˆβ‚_ )

  βŸͺ_∼_⟫-intro : (u v : A) β†’ (proj₁ R) u v β†’ βŸͺ u ⟫{R} β‰ˆβ‚ βŸͺ v ⟫{R}
  βŸͺ u ∼ v ⟫-intro = id

  βŸͺ_∼_⟫-elim : (u v : A) β†’ βŸͺ u ⟫{R} β‰ˆβ‚ βŸͺ v ⟫{R} β†’ (proj₁ R) u v
  βŸͺ u ∼ v ⟫-elim = id

β‰‘β†’βŠ† : {A : Type Ξ±}{ρ : Level}(Q R : Pred A ρ) β†’ Q ≑ R β†’ Q βŠ† R
β‰‘β†’βŠ† Q .Q ≑.refl {x} Qx = Qx