Martin Escardo and Tom de Jong, August 2018, April 2022, September 2023.

Quotients. Much of this material is moved from or abstracted from the
earlier 2018 module Quotient.Large by Martin Escardo.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Quotient.Type where

open import MLTT.Spartan

open import UF.Base hiding (_β_)
open import UF.Equiv
open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.Sets-Properties
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

is-prop-valued is-equiv-relation : {X : π€ Μ } β (X β X β π₯ Μ ) β π€ β π₯ Μ
is-prop-valued    _β_ = β x y β is-prop (x β y)
is-equiv-relation _β_ = is-prop-valued _β_
Γ reflexive      _β_
Γ symmetric      _β_
Γ transitive     _β_

EqRel : {π€ π₯ : Universe} β π€ Μ β π€ β (π₯ βΊ) Μ
EqRel {π€} {π₯} X = Ξ£ R κ (X β X β π₯ Μ ) , is-equiv-relation R

_β[_]_ : {X : π€ Μ } β X β EqRel X β X β π₯ Μ
x β[ _β_ , _ ] y = x β y

identifies-related-points : {X : π€ Μ }
β EqRel {π€} {π₯} X
β {Y : π¦ Μ }
β (X β Y) β π€ β π₯ β π¦ Μ
identifies-related-points (_β_ , _) f = β {x x'} β x β x' β f x οΌ f x'

\end{code}

To account for the module Quotient.Large, and, at the same time, usual
(small) quotients, we introduce a parametric definion of existence of
quotients. For small quotients we take β = id, and for large quotients
we take β = (_βΊ) (see below).

\begin{code}

record general-set-quotients-exist (β : Universe β Universe) : π€Ο where
field
_/_ : {π€ π₯ : Universe} (X : π€ Μ ) β EqRel {π€} {π₯} X β π€ β β π₯ Μ
Ξ·/ : {π€ π₯ : Universe} {X : π€ Μ } (β : EqRel {π€} {π₯} X) β X β X / β
Ξ·/-identifies-related-points : {π€ π₯ : Universe}
{X : π€ Μ } (β : EqRel {π€} {π₯} X)
β identifies-related-points β (Ξ·/ β)
/-is-set : {π€ π₯ : Universe} {X : π€ Μ } (β : EqRel {π€} {π₯} X) β is-set (X / β)
/-universality : {π€ π₯ : Universe} {X : π€ Μ } (β : EqRel {π€} {π₯} X)
{π¦ : Universe} {Y : π¦ Μ }
β is-set Y
β (f : X β Y)
β identifies-related-points β f
β β! fΜ κ (X / β β Y) , fΜ β Ξ·/ β βΌ f

\end{code}

The induction principle follows from the universal property.

\begin{code}

/-induction : {X : π€ Μ } (β : EqRel {π€} {π₯} X)
{P : X / β β π¦ Μ }
β ((x' : X / β) β is-prop (P x'))
β ((x : X) β P (Ξ·/ β x)) β (y : X / β) β P y
/-induction {X = X} β {P} P-is-prop-valued Ο y =
transport P (happly fΜ-section-of-prβ y) (prβ (fΜ y))
where
f : X β Ξ£ P
f x = (Ξ·/ β x , Ο x)
f-identifies-related-points : identifies-related-points β f
f-identifies-related-points r =
to-subtype-οΌ P-is-prop-valued (Ξ·/-identifies-related-points β r)
Ξ£P-is-set : is-set (Ξ£ P)
Ξ£P-is-set = subsets-of-sets-are-sets (X / β) P (/-is-set β)
(Ξ» {x'} β P-is-prop-valued x')
u : β! fΜ κ (X / β β Ξ£ P) , fΜ β Ξ·/ β βΌ f
u = /-universality β Ξ£P-is-set f f-identifies-related-points
fΜ : X / β β Ξ£ P
fΜ = β!-witness u
fΜ-after-Ξ·-is-f : fΜ β Ξ·/ β βΌ f
fΜ-after-Ξ·-is-f = β!-is-witness u
fΜ-section-of-prβ : prβ β fΜ οΌ id
fΜ-section-of-prβ = ap prβ (singletons-are-props c (prβ β fΜ , h)
(id , Ξ» x β refl))
where
c : β! g κ (X / β β X / β) , g β Ξ·/ β βΌ Ξ·/ β
c = /-universality β (/-is-set β) (Ξ·/ β) (Ξ·/-identifies-related-points β)
h : prβ β fΜ β Ξ·/ β βΌ Ξ·/ β
h x = ap prβ (fΜ-after-Ξ·-is-f x)

\end{code}

Paying attention to universe levels, it is important to note that the quotient
of X : π€ by a π₯-valued equivalence relation is assumed to live in π€ β π₯. In
particular, the quotient of type in π€ by a π€-valued equivalence relation lives
in π€ again.

The following are facts about quotients, moved from Quotient.Large as
they are of general use.

\begin{code}

module _
{X : π€ Μ }
(β@(_β_ , βp , βr , βs , βt) : EqRel {π€} {π₯} X)
where

module _ (pt : propositional-truncations-exist) where

open PropositionalTruncation pt
open import UF.ImageAndSurjection pt

Ξ·/-is-surjection : is-surjection (Ξ·/ {π€} {π₯} {X} β)
Ξ·/-is-surjection = /-induction β
(Ξ» x' β being-in-the-image-is-prop x' (Ξ·/ β))
(Ξ» x β β£ x , refl β£)
module _
{A : π¦ Μ }
(A-is-set : is-set A)
where

mediating-map/ : (f : X β A)
β identifies-related-points β f
β X / β β A
mediating-map/ f j = β!-witness (/-universality β A-is-set f j)

universality-triangle/ : (f : X β A)
(j : identifies-related-points β f)
β mediating-map/ f j β Ξ·/ β βΌ f
universality-triangle/ f j = β!-is-witness (/-universality β A-is-set f j)

at-most-one-mediating-map/ : (g h : X / β β A)
β g β Ξ·/ β βΌ h β Ξ·/ β
β g βΌ h
at-most-one-mediating-map/ g h p x = Ξ³
where
f : X β A
f = g β Ξ·/ β

j : identifies-related-points β f
j e = ap g (Ξ·/-identifies-related-points β e)

q : mediating-map/ f j οΌ g
q = witness-uniqueness (Ξ» fΜ β fΜ β Ξ·/ β βΌ f)
(/-universality β A-is-set f j)
(mediating-map/ f j)
g
(universality-triangle/ f j)
(Ξ» x β refl)

r : mediating-map/ f j οΌ h
r = witness-uniqueness (Ξ» fΜ β fΜ β Ξ·/ β βΌ f)
(/-universality β A-is-set f j)
(mediating-map/ f j)
h
(universality-triangle/ f j)
(Ξ» x β (p x)β»ΒΉ)

Ξ³ = g x                  οΌβ¨ happly (q β»ΒΉ) x β©
mediating-map/ f j x οΌβ¨ happly r x β©
h x                  β

extension/ : (f : X β X / β)
β identifies-related-points β f
β (X / β β X / β)
extension/ = mediating-map/ (/-is-set β)

extension-triangle/ : (f : X β X / β)
(i : identifies-related-points β f)
β extension/ f i β Ξ·/ β βΌ f
extension-triangle/ = universality-triangle/ (/-is-set β)

module _ (f : X β X)
(p : {x y : X} β x β y β f x β f y)
where

abstract
private
Ο : identifies-related-points β (Ξ·/ β β f)
Ο e = Ξ·/-identifies-related-points β (p e)

extensionβ/ : X / β β X / β
extensionβ/ = extension/ (Ξ·/ β β f) Ο

naturality/ : extensionβ/ β Ξ·/ β βΌ Ξ·/ β β f
naturality/ = universality-triangle/ (/-is-set β) (Ξ·/ β β f) Ο

module _ (f : X β X β X)
(p : {x y x' y' : X} β x β x' β y β y' β f x y β f x' y')
where

abstract
private
Ο : (x : X) β identifies-related-points β (Ξ·/ β β f x)
Ο x {y} {y'} e = Ξ·/-identifies-related-points β (p {x} {y} {x} {y'} (βr x) e)

p' : (x : X) {y y' : X} β y β y' β f x y β f x y'
p' x {x'} {y'} = p {x} {x'} {x} {y'} (βr x)

fβ : X β X / β β X / β
fβ x = extensionβ/ (f x) (p' x)

Ξ΄ : {x x' : X} β x β x' β (y : X) β fβ x (Ξ·/ β y) οΌ fβ x' (Ξ·/ β y)
Ξ΄ {x} {x'} e y =
fβ x (Ξ·/ β y)   οΌβ¨ naturality/ (f x) (p' x) y β©
Ξ·/ β (f x y)    οΌβ¨ Ξ·/-identifies-related-points β (p e (βr y)) β©
Ξ·/ β (f x' y)   οΌβ¨ (naturality/ (f x') (p' x') y)β»ΒΉ β©
fβ x' (Ξ·/ β y)  β

Ο : (b : X / β) {x x' : X} β x β x' β fβ x b οΌ fβ x' b
Ο b {x} {x'} e = /-induction β (Ξ» y β /-is-set β) (Ξ΄ e) b

fβ : X / β β X / β β X / β
fβ d e = extension/ (Ξ» x β fβ x e) (Ο e) d

extensionβ/ : X / β β X / β β X / β
extensionβ/ = fβ

abstract
naturalityβ/ : (x y : X) β fβ (Ξ·/ β x) (Ξ·/ β y) οΌ Ξ·/ β (f x y)
naturalityβ/ x y =
fβ (Ξ·/ β x) (Ξ·/ β y) οΌβ¨ extension-triangle/ (Ξ» x β fβ x (Ξ·/ β y)) (Ο (Ξ·/ β y)) x β©
fβ x (Ξ·/ β y)        οΌβ¨ naturality/ (f x) (p (βr x)) y β©
Ξ·/ β (f x y)         β

\end{code}

We extend unary and binary prop-valued relations to the quotient.

\begin{code}

module extending-relations-to-quotient (fe : Fun-Ext) (pe : Prop-Ext) where

module _
{X : π€ Μ }
(β@(_β_ , βp , βr , βs , βt) : EqRel {π€} {π₯} X)
where

module _
(r : X β Ξ© π£)
(p : {x y : X} β x β y β r x οΌ r y)
where

extension-relβ : X / β β Ξ© π£
extension-relβ = mediating-map/ β (Ξ©-is-set fe pe) r p

extension-rel-triangleβ : extension-relβ β Ξ·/ β βΌ r
extension-rel-triangleβ = universality-triangle/ β (Ξ©-is-set fe pe) r p

module _ (r : X β X β Ξ© π£)
(p : {x y x' y' : X} β x β x' β y β y' β r x y οΌ r x' y')
where

abstract
private
p' : (x : X) {y y' : X} β y β y' β r x y οΌ r x y'
p' x {y} {y'} = p (βr x)

rβ : X β X / β β Ξ© π£
rβ x = extension-relβ (r x) (p' x)

Ξ΄ : {x x' : X} β x β x' β (y : X) β rβ x (Ξ·/ β y) οΌ rβ x' (Ξ·/ β y)
Ξ΄ {x} {x'} e y =
rβ x  (Ξ·/ β y)  οΌβ¨ extension-rel-triangleβ (r x) (p (βr x)) y        β©
r  x     y      οΌβ¨ p e (βr y)                                        β©
r  x'    y      οΌβ¨ (extension-rel-triangleβ (r x') (p (βr x')) y) β»ΒΉ β©
rβ x' (Ξ·/ β y)  β

Ο : (q : X / β) {x x' : X} β x β x' β rβ x q οΌ rβ x' q
Ο q {x} {x'} e = /-induction β (Ξ» q β Ξ©-is-set fe pe) (Ξ΄ e) q

rβ : X / β β X / β β Ξ© π£
rβ = mediating-map/ β (Ξ -is-set fe (Ξ» _ β Ξ©-is-set fe pe)) rβ
(Ξ» {x} {x'} e β dfunext fe (Ξ» q β Ο q e))

Ο : (x : X) β rβ (Ξ·/ β x) οΌ rβ x
Ο = universality-triangle/ β (Ξ -is-set fe (Ξ» _ β Ξ©-is-set fe pe)) rβ
(Ξ» {x} {x'} e β dfunext fe (Ξ» q β Ο q e))

Ο : (x y : X) β rβ (Ξ·/ β x) (Ξ·/ β y) οΌ r x y
Ο x y = rβ (Ξ·/ β x) (Ξ·/ β y) οΌβ¨ happly (Ο x) (Ξ·/ β y) β©
rβ x        (Ξ·/ β y) οΌβ¨ extension-rel-triangleβ (r x) (p' x) y β©
r  x            y    β

extension-relβ : X / β β X / β β Ξ© π£
extension-relβ = rβ

extension-rel-triangleβ : (x y : X)
β extension-relβ (Ξ·/ β x) (Ξ·/ β y) οΌ r x y
extension-rel-triangleβ = Ο

\end{code}

For proving properties of an extended binary relation, it is useful to have a
binary and ternary versions of quotient induction.

\begin{code}

module _
(fe : Fun-Ext)
{X : π€ Μ }
(β : EqRel {π€ } {π₯} X)
where

/-inductionβ : β {π¦} {P : X / β β X / β β π¦ Μ }
β ((x' y' : X / β) β is-prop (P x' y'))
β ((x y : X) β P (Ξ·/ β x) (Ξ·/ β y))
β (x' y' : X / β) β P x' y'
/-inductionβ p h =
/-induction β (Ξ» x' β Ξ -is-prop fe (p x'))
(Ξ» x β /-induction β (p (Ξ·/ β x)) (h x))

/-inductionβ : β {π¦} β {P : X / β β X / β β X / β β π¦ Μ }
β ((x' y' z' : X / β) β is-prop (P x' y' z'))
β ((x y z : X) β P (Ξ·/ β x) (Ξ·/ β y) (Ξ·/ β z))
β (x' y' z' : X / β) β P x' y' z'
/-inductionβ p h =
/-inductionβ (Ξ» x' y' β Ξ -is-prop fe (p x' y'))
(Ξ» x y β /-induction β (p (Ξ·/ β x) (Ξ·/ β y)) (h x y))

quotients-equivalent : (X : π€ Μ ) (R : EqRel {π€} {π₯} X) (R' : EqRel {π€} {π¦} X)
β ({x y : X} β x β[ R ] y β x β[ R' ] y)
β (X / R) β (X / R')
quotients-equivalent X (_β_  , βp ,  βr  , βs  , βt )
(_β'_ , βp' , βr' , βs' , βt') Ξ΅ = Ξ³
where
β  = (_β_  , βp ,  βr  , βs  , βt )
β' = (_β'_ , βp' , βr' , βs' , βt')
i : {x y : X} β x β y β Ξ·/ β' x οΌ Ξ·/ β' y
i e = Ξ·/-identifies-related-points β' (lr-implication Ξ΅ e)
iβ»ΒΉ : {x y : X} β x β' y β Ξ·/ β x οΌ Ξ·/ β y
iβ»ΒΉ e = Ξ·/-identifies-related-points β (rl-implication Ξ΅ e)
f : X / β β X / β'
f = mediating-map/ β (/-is-set β') (Ξ·/ β') i
fβ»ΒΉ : X / β' β X / β
fβ»ΒΉ = mediating-map/ β' (/-is-set β) (Ξ·/ β) iβ»ΒΉ
a : (x : X) β f (fβ»ΒΉ (Ξ·/ β' x)) οΌ Ξ·/ β' x
a x = f (fβ»ΒΉ (Ξ·/ β' x)) οΌβ¨ I β©
f (Ξ·/ β x)        οΌβ¨ II β©
Ξ·/ β' x           β
where
I  = ap f (universality-triangle/ β' (/-is-set β) (Ξ·/ β) iβ»ΒΉ x)
II = universality-triangle/ β (/-is-set β') (Ξ·/ β') i x
Ξ± : f β fβ»ΒΉ βΌ id
Ξ± = /-induction β' (Ξ» _ β /-is-set β') a
b : (x : X) β fβ»ΒΉ (f (Ξ·/ β x)) οΌ Ξ·/ β x
b x = fβ»ΒΉ (f (Ξ·/ β x)) οΌβ¨ I β©
fβ»ΒΉ (Ξ·/ β' x)    οΌβ¨ II β©
Ξ·/ β x           β
where
I  = ap fβ»ΒΉ (universality-triangle/ β (/-is-set β') (Ξ·/ β') i x)
II = universality-triangle/ β' (/-is-set β) (Ξ·/ β) iβ»ΒΉ x
Ξ² : fβ»ΒΉ β f βΌ id
Ξ² = /-induction β (Ξ» _ β /-is-set β) b
Ξ³ : (X / β) β (X / β')
Ξ³ = qinveq f (fβ»ΒΉ , Ξ² , Ξ±)

\end{code}

We now define the existence of small and large quotients:

\begin{code}

set-quotients-exist large-set-quotients-exist : π€Ο
set-quotients-exist       = general-set-quotients-exist (Ξ» π€ β π€)
large-set-quotients-exist = general-set-quotients-exist (_βΊ)

\end{code}

It turns out that quotients, if they exist, are necessarily
effective. This is proved the module Quotient.Effective. But we need
to include the definition here.

\begin{code}

are-effective : {β : Universe β Universe} β general-set-quotients-exist β β π€Ο
are-effective sq = {π€ π₯ : Universe} {X : π€ Μ }
(R : EqRel {π€} {π₯} X)
{x y : X}
β Ξ·/ R x οΌ Ξ·/ R y β x β[ R ] y
where
open general-set-quotients-exist sq

\end{code}