# Functoriality of set quotients

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Eléonore Mangel, Elisabeth Stenholm, Daniel Gratzer, Julian KG, fernabnor and louismntnu.

Created on 2022-02-17.

{-# OPTIONS --lossy-unification #-}

module foundation.functoriality-set-quotients where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalence-extensionality
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopy-induction
open import foundation.logical-equivalences
open import foundation.reflecting-maps-equivalence-relations
open import foundation.set-quotients
open import foundation.subtype-identity-principle
open import foundation.surjective-maps
open import foundation.uniqueness-set-quotients
open import foundation.universal-property-set-quotients
open import foundation.universe-levels

open import foundation-core.commuting-squares-of-maps
open import foundation-core.contractible-types
open import foundation-core.equivalence-relations
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.sets
open import foundation-core.subtypes
open import foundation-core.torsorial-type-families


## Idea

Set quotients act functorially on types equipped with equivalence relations.

## Definition

### Maps preserving equivalence relations

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} (R : equivalence-relation l2 A)
{B : UU l3} (S : equivalence-relation l4 B)
where

preserves-sim-prop-equivalence-relation : (f : A → B) → Prop (l1 ⊔ l2 ⊔ l4)
preserves-sim-prop-equivalence-relation f =
implicit-Π-Prop A
( λ x →
implicit-Π-Prop A
( λ y →
function-Prop
( sim-equivalence-relation R x y)
( prop-equivalence-relation S (f x) (f y))))

preserves-sim-equivalence-relation : (f : A → B) → UU (l1 ⊔ l2 ⊔ l4)
preserves-sim-equivalence-relation f =
type-Prop (preserves-sim-prop-equivalence-relation f)

is-prop-preserves-sim-equivalence-relation :
(f : A → B) → is-prop (preserves-sim-equivalence-relation f)
is-prop-preserves-sim-equivalence-relation f =
is-prop-type-Prop (preserves-sim-prop-equivalence-relation f)

hom-equivalence-relation : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
hom-equivalence-relation =
type-subtype preserves-sim-prop-equivalence-relation

map-hom-equivalence-relation : hom-equivalence-relation → A → B
map-hom-equivalence-relation = pr1

preserves-sim-hom-equivalence-relation :
(f : hom-equivalence-relation) {x y : A} →
sim-equivalence-relation R x y →
sim-equivalence-relation
( S)
( map-hom-equivalence-relation f x)
( map-hom-equivalence-relation f y)
preserves-sim-hom-equivalence-relation = pr2

id-hom-equivalence-relation :
{l1 l2 : Level} {A : UU l1}
(R : equivalence-relation l2 A) →
hom-equivalence-relation R R
pr1 (id-hom-equivalence-relation R) = id
pr2 (id-hom-equivalence-relation R) = id


### Equivalences preserving equivalence relations

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} (R : equivalence-relation l2 A)
{B : UU l3} (S : equivalence-relation l4 B)
where

equiv-equivalence-relation : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
equiv-equivalence-relation =
Σ ( A ≃ B)
( λ e →
{x y : A} →
sim-equivalence-relation R x y ↔
sim-equivalence-relation S (map-equiv e x) (map-equiv e y))

equiv-equiv-equivalence-relation : equiv-equivalence-relation → A ≃ B
equiv-equiv-equivalence-relation = pr1

map-equiv-equivalence-relation : equiv-equivalence-relation → A → B
map-equiv-equivalence-relation e =
map-equiv (equiv-equiv-equivalence-relation e)

map-inv-equiv-equivalence-relation : equiv-equivalence-relation → B → A
map-inv-equiv-equivalence-relation e =
map-inv-equiv (equiv-equiv-equivalence-relation e)

is-equiv-map-equiv-equivalence-relation :
(e : equiv-equivalence-relation) →
is-equiv (map-equiv-equivalence-relation e)
is-equiv-map-equiv-equivalence-relation e =
is-equiv-map-equiv (equiv-equiv-equivalence-relation e)

equiv-sim-equiv-equivalence-relation :
(e : equiv-equivalence-relation) {x y : A} →
sim-equivalence-relation R x y ↔
sim-equivalence-relation
( S)
( map-equiv-equivalence-relation e x)
( map-equiv-equivalence-relation e y)
equiv-sim-equiv-equivalence-relation = pr2

preserves-sim-equiv-equivalence-relation :
(e : equiv-equivalence-relation) {x y : A} →
sim-equivalence-relation R x y →
sim-equivalence-relation
( S)
( map-equiv-equivalence-relation e x)
( map-equiv-equivalence-relation e y)
preserves-sim-equiv-equivalence-relation e =
pr1 (equiv-sim-equiv-equivalence-relation e)

hom-equiv-equivalence-relation :
equiv-equivalence-relation → hom-equivalence-relation R S
pr1 (hom-equiv-equivalence-relation e) = map-equiv-equivalence-relation e
pr2 (hom-equiv-equivalence-relation e) =
preserves-sim-equiv-equivalence-relation e

id-equiv-equivalence-relation :
{l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A) →
equiv-equivalence-relation R R
pr1 (id-equiv-equivalence-relation R) = id-equiv
pr1 (pr2 (id-equiv-equivalence-relation R)) = id
pr2 (pr2 (id-equiv-equivalence-relation R)) = id


### Maps between types satisfying the universal property of set quotients

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} (R : equivalence-relation l2 A)
(QR : Set l3) (f : reflecting-map-equivalence-relation R (type-Set QR))
{B : UU l4} (S : equivalence-relation l5 B)
(QS : Set l6) (g : reflecting-map-equivalence-relation S (type-Set QS))
where

unique-map-is-set-quotient :
is-set-quotient R QR f → is-set-quotient S QS g →
(h : hom-equivalence-relation R S) →
is-contr
( Σ ( type-Set QR → type-Set QS)
( coherence-square-maps
( map-hom-equivalence-relation R S h)
( map-reflecting-map-equivalence-relation R f)
( map-reflecting-map-equivalence-relation S g)))
unique-map-is-set-quotient Uf Ug h =
universal-property-set-quotient-is-set-quotient R QR f Uf QS
( pair
( map-reflecting-map-equivalence-relation S g ∘
map-hom-equivalence-relation R S h)
( λ r →
reflects-map-reflecting-map-equivalence-relation S g
( preserves-sim-hom-equivalence-relation R S h r)))

map-is-set-quotient :
is-set-quotient R QR f → is-set-quotient S QS g →
(h : hom-equivalence-relation R S) →
type-Set QR → type-Set QS
map-is-set-quotient Uf Ug h =
pr1 (center (unique-map-is-set-quotient Uf Ug h))

coherence-square-map-is-set-quotient :
(Uf : is-set-quotient R QR f) →
(Ug : is-set-quotient S QS g) →
(h : hom-equivalence-relation R S) →
coherence-square-maps
( map-hom-equivalence-relation R S h)
( map-reflecting-map-equivalence-relation R f)
( map-reflecting-map-equivalence-relation S g)
( map-is-set-quotient Uf Ug h)
coherence-square-map-is-set-quotient Uf Ug h =
pr2 (center (unique-map-is-set-quotient Uf Ug h))


### Functoriality of the set quotient

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} (R : equivalence-relation l2 A)
{B : UU l3} (S : equivalence-relation l4 B)
where

unique-map-set-quotient :
(h : hom-equivalence-relation R S) →
is-contr
( Σ ( set-quotient R → set-quotient S)
( coherence-square-maps
( map-hom-equivalence-relation R S h)
( quotient-map R)
( quotient-map S)))
unique-map-set-quotient =
unique-map-is-set-quotient
( R)
( quotient-Set R)
( reflecting-map-quotient-map R)
( S)
( quotient-Set S)
( reflecting-map-quotient-map S)
( is-set-quotient-set-quotient R)
( is-set-quotient-set-quotient S)

map-set-quotient :
(h : hom-equivalence-relation R S) → set-quotient R → set-quotient S
map-set-quotient =
map-is-set-quotient
( R)
( quotient-Set R)
( reflecting-map-quotient-map R)
( S)
( quotient-Set S)
( reflecting-map-quotient-map S)
( is-set-quotient-set-quotient R)
( is-set-quotient-set-quotient S)

coherence-square-map-set-quotient :
(h : hom-equivalence-relation R S) →
coherence-square-maps
( map-hom-equivalence-relation R S h)
( quotient-map R)
( quotient-map S)
( map-set-quotient h)
coherence-square-map-set-quotient =
coherence-square-map-is-set-quotient
( R)
( quotient-Set R)
( reflecting-map-quotient-map R)
( S)
( quotient-Set S)
( reflecting-map-quotient-map S)
( is-set-quotient-set-quotient R)
( is-set-quotient-set-quotient S)


## Properties

### Composition of reflecting maps

module _
{l1 l2 l3 l4 l5 : Level}
{A : UU l1} (R : equivalence-relation l2 A)
{B : UU l3} (S : equivalence-relation l4 B)
{C : UU l5}
where

comp-reflecting-map-equivalence-relation :
reflecting-map-equivalence-relation S C → hom-equivalence-relation R S →
reflecting-map-equivalence-relation R C
pr1 (comp-reflecting-map-equivalence-relation g f) =
map-reflecting-map-equivalence-relation S g ∘
map-hom-equivalence-relation R S f
pr2 (comp-reflecting-map-equivalence-relation g f) r =
reflects-map-reflecting-map-equivalence-relation S g
( preserves-sim-hom-equivalence-relation R S f r)


### Characterizing equality of hom-equivalence-relation

module _
{l1 l2 l3 l4 : Level}
{A : UU l1} (R : equivalence-relation l2 A)
{B : UU l3} (S : equivalence-relation l4 B)
where

htpy-hom-equivalence-relation :
(f g : hom-equivalence-relation R S) → UU (l1 ⊔ l3)
htpy-hom-equivalence-relation f g =
map-hom-equivalence-relation R S f ~ map-hom-equivalence-relation R S g

refl-htpy-hom-equivalence-relation :
(f : hom-equivalence-relation R S) → htpy-hom-equivalence-relation f f
refl-htpy-hom-equivalence-relation f = refl-htpy

htpy-eq-hom-equivalence-relation :
(f g : hom-equivalence-relation R S) →
(f ＝ g) → htpy-hom-equivalence-relation f g
htpy-eq-hom-equivalence-relation f .f refl =
refl-htpy-hom-equivalence-relation f

is-torsorial-htpy-hom-equivalence-relation :
(f : hom-equivalence-relation R S) →
is-torsorial (htpy-hom-equivalence-relation f)
is-torsorial-htpy-hom-equivalence-relation f =
is-torsorial-Eq-subtype
( is-torsorial-htpy (map-hom-equivalence-relation R S f))
( is-prop-preserves-sim-equivalence-relation R S)
( map-hom-equivalence-relation R S f)
( refl-htpy-hom-equivalence-relation f)
( preserves-sim-hom-equivalence-relation R S f)

is-equiv-htpy-eq-hom-equivalence-relation :
(f g : hom-equivalence-relation R S) →
is-equiv (htpy-eq-hom-equivalence-relation f g)
is-equiv-htpy-eq-hom-equivalence-relation f =
fundamental-theorem-id
( is-torsorial-htpy-hom-equivalence-relation f)
( htpy-eq-hom-equivalence-relation f)

extensionality-hom-equivalence-relation :
(f g : hom-equivalence-relation R S) →
(f ＝ g) ≃ htpy-hom-equivalence-relation f g
pr1 (extensionality-hom-equivalence-relation f g) =
htpy-eq-hom-equivalence-relation f g
pr2 (extensionality-hom-equivalence-relation f g) =
is-equiv-htpy-eq-hom-equivalence-relation f g

eq-htpy-hom-equivalence-relation :
(f g : hom-equivalence-relation R S) →
htpy-hom-equivalence-relation f g → (f ＝ g)
eq-htpy-hom-equivalence-relation f g =
map-inv-equiv (extensionality-hom-equivalence-relation f g)


### Functoriality of set quotients preserves equivalences

module _
{l1 l2 l3 l4 l5 l6 : Level}
{A : UU l1} (R : equivalence-relation l2 A)
(QR : Set l3) (f : reflecting-map-equivalence-relation R (type-Set QR))
{B : UU l4} (S : equivalence-relation l5 B)
(QS : Set l6) (g : reflecting-map-equivalence-relation S (type-Set QS))
where

unique-equiv-is-set-quotient :
is-set-quotient R QR f → is-set-quotient S QS g →
(h : equiv-equivalence-relation R S) →
is-contr
( Σ ( type-Set QR ≃ type-Set QS)
( λ h' →
coherence-square-maps
( map-equiv-equivalence-relation R S h)
( map-reflecting-map-equivalence-relation R f)
( map-reflecting-map-equivalence-relation S g)
( map-equiv h')))
unique-equiv-is-set-quotient Uf Ug h =
uniqueness-set-quotient R QR f Uf QS
( comp-reflecting-map-equivalence-relation R S g
( hom-equiv-equivalence-relation R S h))
( is-set-quotient-is-surjective-and-effective R QS
( comp-reflecting-map-equivalence-relation R S g
( hom-equiv-equivalence-relation R S h))
( ( is-surjective-comp
( is-surjective-is-set-quotient S QS g Ug)
( is-surjective-is-equiv
( is-equiv-map-equiv-equivalence-relation R S h))) ,
( λ x y →
( inv-equiv
( equiv-iff'
( prop-equivalence-relation R x y)
( prop-equivalence-relation S
( map-equiv-equivalence-relation R S h x)
( map-equiv-equivalence-relation R S h y))
( equiv-sim-equiv-equivalence-relation R S h))) ∘e
( is-effective-is-set-quotient S QS g Ug
( map-equiv-equivalence-relation R S h x)
( map-equiv-equivalence-relation R S h y)))))

equiv-is-set-quotient :
is-set-quotient R QR f →
is-set-quotient S QS g →
(h : equiv-equivalence-relation R S) → type-Set QR ≃ type-Set QS
equiv-is-set-quotient Uf Ug h =
pr1 (center (unique-equiv-is-set-quotient Uf Ug h))

coherence-square-equiv-is-set-quotient :
(Uf : is-set-quotient R QR f) →
(Ug : is-set-quotient S QS g) →
(h : equiv-equivalence-relation R S) →
coherence-square-maps (map-equiv-equivalence-relation R S h)
( map-reflecting-map-equivalence-relation R f)
( map-reflecting-map-equivalence-relation S g)
( map-equiv (equiv-is-set-quotient Uf Ug h))
coherence-square-equiv-is-set-quotient Uf Ug h =
pr2 (center (unique-equiv-is-set-quotient Uf Ug h))


### Functoriality of set quotients preserves identity maps

module _
{l1 l2 l3 : Level}
{A : UU l1} (R : equivalence-relation l2 A)
(QR : Set l3) (f : reflecting-map-equivalence-relation R (type-Set QR))
where

id-map-is-set-quotient :
(Uf : is-set-quotient R QR f) →
map-is-set-quotient R QR f R QR f Uf Uf (id-hom-equivalence-relation R) ~ id
id-map-is-set-quotient Uf x =
ap
( λ c → pr1 c x)
{ x =
center
( unique-map-is-set-quotient
R QR f R QR f Uf Uf (id-hom-equivalence-relation R))}
{ y = pair id refl-htpy}
( eq-is-contr
( unique-map-is-set-quotient
R QR f R QR f Uf Uf (id-hom-equivalence-relation R)))

id-equiv-is-set-quotient :
(Uf : is-set-quotient R QR f) →
htpy-equiv
( equiv-is-set-quotient R QR f R QR f Uf Uf
( id-equiv-equivalence-relation R))
( id-equiv)
id-equiv-is-set-quotient Uf x =
ap
( λ c → map-equiv (pr1 c) x)
{ x =
center
( unique-equiv-is-set-quotient R QR f R QR f Uf Uf
( id-equiv-equivalence-relation R))}
{ y = pair id-equiv refl-htpy}
( eq-is-contr
( unique-equiv-is-set-quotient R QR f R QR f Uf Uf
( id-equiv-equivalence-relation R)))