Tom de Jong, 4 & 5 April 2022.

Assuming set quotients, we
(1) derive propositional truncations in the presence of function extensionality;
(2) prove Set Replacement as defined in UF.Size.lagda.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-}

module UF.Quotient 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.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Size

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'

record set-quotients-exist : π€Ο 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')
F : β! fΜ κ (X / β β Ξ£ P) , fΜ β Ξ·/ β βΌ f
F = /-universality β Ξ£P-is-set f f-identifies-related-points
fΜ : X / β β Ξ£ P
fΜ = β!-witness F
fΜ-after-Ξ·-is-f : fΜ β Ξ·/ β βΌ f
fΜ-after-Ξ·-is-f = β!-is-witness F
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 is boilerplate and duplicates some of the material in
UF.Quotient.lagda, where large set quotients are constructed using propositional
truncations, function extensionality and propositional extensionality.

We need the boilerplate in OrdinalOfOrdinalsSuprema.lagda, where we use set
quotients to construct small suprema of small ordinals.

A quotient is said to be effective if for every x, y : X, we have x β y whenever
Ξ·/ x οΌ βΞ·/ y. Notice that we did not include effectivity as a requirement in
'set-quotients-exist'. But actually it follows from the other properties, at
least in the presence of function extensionality and propositonal
extensionality, as MartΓ­n observed. The proof is as follows:

(1) First construct propositional truncations using assumed set quotients.
(2) Construct another (large) quotient as described in UF.Large-Quotients.lagda.
(3) This large quotient is effective, but has to be isomorphic to the assumed
set quotient, hence this quotient has to be effective as well.

TODO: Implement this in Agda.

\begin{code}

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

module _
{A : π¦ Μ  }
(A-is-set : is-set A)
where

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

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

\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
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'
Ξ³ : (X / β) β (X / β')
Ξ³ = qinveq f (f' , Ξ±' , Ξ±)

\end{code}

We now construct propositional truncations using set quotients. Notice that
function extensionality is (only) needed to prove that the quotient is a
proposition.

\begin{code}

private
module _ {X : π€ Μ  } where
_β_ : X β X β π€β Μ
x β y = π
β : EqRel X
β = _β_ , (Ξ» x y β π-is-prop) , (Ξ» x β β) , (Ξ» x y _ β β) , (Ξ» x y z _ _ β β)

β₯_β₯ : π€ Μ  β π€ Μ
β₯_β₯ X = X / β

β£_β£ : {X : π€ Μ  } β X β β₯ X β₯
β£_β£ = Ξ·/ β

β₯β₯-is-prop : {X : π€ Μ  } β funext π€ π€ β is-prop β₯ X β₯
β₯β₯-is-prop {π€} {X} fe = /-induction β (Ξ» x' β Ξ -is-prop fe (Ξ» y' β /-is-set β))
(Ξ» x β /-induction β (Ξ» y' β /-is-set β)
(Ξ» y β Ξ·/-identifies-related-points β β))

β₯β₯-rec : {X : π€ Μ  } {P : π₯ Μ  } β is-prop P β (X β P) β β₯ X β₯ β P
β₯β₯-rec {π€} {π₯} {X} {P} i f =
β!-witness (/-universality β (props-are-sets i) f
(Ξ» {x} {x'}_ β i (f x) (f x')))

propositional-truncations-from-set-quotients :
Fun-Ext β propositional-truncations-exist
propositional-truncations-from-set-quotients fe = record
{ β₯_β₯        = β₯_β₯
; β₯β₯-is-prop = β₯β₯-is-prop fe
; β£_β£        = β£_β£
; β₯β₯-rec     = β₯β₯-rec
}

\end{code}

Finally, we show that Set Replacement is derivable when we have set quotients as
defined above.

Notice how we could replace propositional-truncations-exist assumption by
function extensionality (funext) as we can use funext to construct truncations,
as shown above.

\begin{code}

module _
(sq : set-quotients-exist)
(pt : propositional-truncations-exist)
where
open set-quotients-exist sq

open PropositionalTruncation pt
open import UF.ImageAndSurjection pt

module set-replacement-construction
{X : π€ Μ  }
{Y : π¦ Μ  }
(f : X β Y)
(Y-is-loc-small : Y is-locally π₯ small)
(Y-is-set : is-set Y)
where

_β_ : X β X β π¦ Μ
x β x' = f x οΌ f x'

β-is-prop-valued : is-prop-valued _β_
β-is-prop-valued x x' = Y-is-set

β-is-reflexive : reflexive _β_
β-is-reflexive x = refl

β-is-symmetric : symmetric _β_
β-is-symmetric x x' p = p β»ΒΉ

β-is-transitive : transitive _β_
β-is-transitive _ _ _ p q = p β q

β-is-equiv-rel : is-equiv-relation _β_
β-is-equiv-rel = β-is-prop-valued , β-is-reflexive  ,
β-is-symmetric   , β-is-transitive

\end{code}

Using that Y is locally π₯ small, we resize _β_ to a π₯-valued equivalence
relation.

\begin{code}

_ββ»_ : X β X β π₯ Μ
x ββ» x' = prβ (Y-is-loc-small (f x) (f x'))

ββ»-β-β : {x x' : X} β x ββ» x' β x β x'
ββ»-β-β {x} {x'} = prβ (Y-is-loc-small (f x) (f x'))

ββ»-is-prop-valued : is-prop-valued _ββ»_
ββ»-is-prop-valued x x' = equiv-to-prop ββ»-β-β (β-is-prop-valued x x')

ββ»-is-reflexive : reflexive _ββ»_
ββ»-is-reflexive x = β ββ»-β-β ββ»ΒΉ (β-is-reflexive x)

ββ»-is-symmetric : symmetric _ββ»_
ββ»-is-symmetric x x' p = β ββ»-β-β ββ»ΒΉ (β-is-symmetric x x' (β ββ»-β-β β p))

ββ»-is-transitive : transitive _ββ»_
ββ»-is-transitive x x' x'' p q =
β ββ»-β-β ββ»ΒΉ (β-is-transitive x x' x'' (β ββ»-β-β β p) (β ββ»-β-β β q))

ββ»-is-equiv-rel : is-equiv-relation _ββ»_
ββ»-is-equiv-rel = ββ»-is-prop-valued , ββ»-is-reflexive  ,
ββ»-is-symmetric   , ββ»-is-transitive

β : EqRel X
β = _β_ , β-is-equiv-rel

X/β : π€ β π¦ Μ
X/β = (X / β)

X/ββ» : π€ β π₯ Μ
X/ββ» = (X / (_ββ»_ , ββ»-is-equiv-rel))

[_] : X β X/β
[_] = Ξ·/ β

X/β-β-X/ββ» : X/β β X/ββ»
X/β-β-X/ββ» = quotients-equivalent X β (_ββ»_ , ββ»-is-equiv-rel)
(β ββ»-β-β ββ»ΒΉ , β ββ»-β-β β)

\end{code}

We now proceed to show that X/β and image f are equivalent types.

\begin{code}

corestriction-respects-β : {x x' : X}
β x β x'
β corestriction f x οΌ corestriction f x'
corestriction-respects-β =
to-subtype-οΌ (Ξ» y β being-in-the-image-is-prop y f)

quotient-to-image : X/β β image f
quotient-to-image = mediating-map/ β (image-is-set f Y-is-set)
(corestriction f) (corestriction-respects-β)

image-to-quotient' : (y : image f)
β Ξ£ q κ X/β , β x κ X , ([ x ] οΌ q) Γ (f x οΌ prβ y)
image-to-quotient' (y , p) = β₯β₯-rec prp r p
where
r : (Ξ£ x κ X , f x οΌ y)
β (Ξ£ q κ X/β , β x κ X , ([ x ] οΌ q) Γ (f x οΌ y))
r (x , e) = [ x ] , β£ x , refl , e β£
prp : is-prop (Ξ£ q κ X/β , β x κ X , ([ x ] οΌ q) Γ (f x οΌ y))
prp (q , u) (q' , u') = to-subtype-οΌ (Ξ» _ β β-is-prop)
(β₯β₯-recβ (/-is-set β) Ξ³ u u')
where
Ξ³ : (Ξ£ x  κ X , ([ x  ] οΌ q ) Γ (f x  οΌ y))
β (Ξ£ x' κ X , ([ x' ] οΌ q') Γ (f x' οΌ y))
β q οΌ q'
Ξ³ (x , refl , e) (x' , refl , refl) = Ξ·/-identifies-related-points β e

image-to-quotient : image f β X/β
image-to-quotient y = prβ (image-to-quotient' y)

image-to-quotient-lemma : (x : X)
β image-to-quotient (corestriction f x) οΌ [ x ]
image-to-quotient-lemma x = β₯β₯-rec (/-is-set β) Ξ³ t
where
q : X/β
q = image-to-quotient (corestriction f x)
t : β x' κ X , ([ x' ] οΌ q) Γ (f x' οΌ f x)
t = prβ (image-to-quotient' (corestriction f x))
Ξ³ : (Ξ£ x' κ X , ([ x' ] οΌ q) Γ (f x' οΌ f x))
β q οΌ [ x ]
Ξ³ (x' , u , v) =   q    οΌβ¨ u β»ΒΉ β©
[ x' ] οΌβ¨ Ξ·/-identifies-related-points β v β©
[ x  ] β

image-β-quotient : image f β X/β
image-β-quotient = qinveq Ο (Ο , Ο , Ο)
where
Ο : image f β X/β
Ο = image-to-quotient
Ο : X/β β image f
Ο = quotient-to-image
Ο : (x : X) β Ο [ x ] οΌ corestriction f x
Ο = universality-triangle/ β (image-is-set f Y-is-set)
(corestriction f)
corestriction-respects-β
Ο : Ο β Ο βΌ id
Ο = /-induction β (Ξ» x' β /-is-set β) Ξ³
where
Ξ³ : (x : X) β Ο (Ο [ x ]) οΌ [ x ]
Ξ³ x = Ο (Ο [ x ])            οΌβ¨ ap Ο (Ο x)                β©
Ο (corestriction f x ) οΌβ¨ image-to-quotient-lemma x β©
[ x ]                  β
Ο : Ο β Ο βΌ id
Ο (y , p) = β₯β₯-rec (image-is-set f Y-is-set) Ξ³ p
where
Ξ³ : (Ξ£ x κ X , f x οΌ y) β Ο (Ο (y , p)) οΌ (y , p)
Ξ³ (x , refl) = Ο (Ο (f x , p))           οΌβ¨ β¦1β¦ β©
Ο (Ο (corestriction f x)) οΌβ¨ β¦2β¦ β©
Ο [ x ]                   οΌβ¨ β¦3β¦ β©
corestriction f x         οΌβ¨ β¦4β¦ β©
(f x , p)                 β
where
β¦4β¦ = to-subtype-οΌ (Ξ» yΒ β being-in-the-image-is-prop y f) refl
β¦1β¦ = ap (Ο β Ο) (β¦4β¦ β»ΒΉ)
β¦2β¦ = ap Ο (image-to-quotient-lemma x)
β¦3β¦ = Ο x

set-replacement-from-set-quotients : Set-Replacement pt
set-replacement-from-set-quotients
{π¦} {π£} {π€} {π₯} {X} {Y} f X-is-small Y-is-loc-small Y-is-set = X/ββ» , β-sym e
where
X' : π€ Μ
X' = prβ X-is-small
Ο : X' β X
Ο = prβ X-is-small
f' : X' β Y
f' = f β β Ο β
open set-replacement-construction f' Y-is-loc-small Y-is-set
open import UF.EquivalenceExamples
e = image f  ββ¨ Ξ£-cong (Ξ» y β β₯β₯-cong pt (h y)) β©