Tom de Jong, 4 & 5 April 2022.

Set Replacement is derivable from the existence of quotients in the
presence of propositional truncations or function extensionality.

\begin{code}

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

module Quotient.GivesSetReplacement where

open import MLTT.Spartan

open import Quotient.Type
open import Quotient.GivesPropTrunc

open import UF.Equiv
open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.Size
open import UF.Subsingletons

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

open general-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-and-prop-trunc : Set-Replacement pt
set-replacement-from-set-quotients-and-prop-trunc
{π¦} {π£} {π€} {π₯} {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)) β©
X/ββ»     β
where
h : (y : Y) β (Ξ£ x κ X , f x οΌ y) β (Ξ£ x' κ X' , f' x' οΌ y)
h y = β-sym (Ξ£-change-of-variable (Ξ» x β f x οΌ y) β Ο β (ββ-is-equiv Ο))

\end{code}

End of anonymous module assuming set-quotients-exist and
propositional-truncations-exist.

\begin{code}

set-replacement-from-set-quotients-and-funext
: (sq : set-quotients-exist)
(fe : Fun-Ext)
β Set-Replacement (propositional-truncations-from-set-quotients sq fe)
set-replacement-from-set-quotients-and-funext sq fe =
set-replacement-from-set-quotients-and-prop-trunc sq
(propositional-truncations-from-set-quotients sq fe)

\end{code}