Skip to content

Setoid.Relations.Quotients

Quotients of setoids

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

Quotienting is where the setoid formulation pays for itself. A quotient of a setoid by an equivalence relation keeps the same carrier and changes only the equality, so it needs neither a quotient type nor any axiom: _/_ takes a type together with an Equivalence bundle and returns the setoid whose equality is that relation, and Quotient is the type of its classes.

The module also supplies what makes quotients reachable in practice: ker-IsEquivalence, that the kernel of a setoid function is an equivalence relation, so that every kernel may be quotiented by; and the machinery of equivalence classes and blocks. The algebraic counterpart, where the quotient must respect the operations as well, is _β•±_ of Setoid.Congruences.Basic.

{-# 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