# Library HoTT.Colimits.Quotient

Require Import Basics.
Require Import Types.
Require Import HSet.
Require Import HProp.
Require Import TruncType.
Require Import HIT.epi.
Require Import HIT.Coeq.
Require Import Truncations.

Local Open Scope path_scope.

# Quotient of a Type by an hprop-valued Relation

We aim to model:
```Inductive Quotient R : Type :=
| class_of R : A -> Quotient R
| qglue : forall x y, (R x y) -> class_of R x = class_of R y
| ishset_quotient : IsHSet (Quotient R)
```
We do this by defining the quotient as a truncated coequalizer.

Definition Quotient@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : Type@{k}
:= Trunc@{k} 0 (Coeq@{k k}
(fun x : sig@{k k} (fun a : Asig (R a)) ⇒ x.1)
(fun x : sig@{k k} (fun a : Asig (R a)) ⇒ x.2.1)).

Definition class_of@{i j k} {A : Type@{i}} (R : Relation@{i j} A)
: A Quotient@{i j k} R := tr o coeq.

Definition qglue@{i j k} {A : Type@{i}} {R : Relation@{i j} A}
{x y : A}
: R x y class_of@{i j k} R x = class_of R y
:= fun pap tr (cglue (x; y; p)).

Global Instance ishset_quotient {A : Type} (R : Relation A)
: IsHSet (Quotient R) := _.

Definition Quotient_ind@{i j k l}
{A : Type@{i}} (R : Relation@{i j} A)
(P : Quotient@{i j k} R Type@{l}) {sP : x, IsHSet (P x)}
(pclass : x, P (class_of R x))
(peq : x y (H : R x y), qglue H # pclass x = pclass y)
: q, P q.
Proof.
eapply Trunc_ind, Coeq_ind.
1: assumption.
intros [a [b p]].
refine (transport_compose _ _ _ _ @ _).
apply peq.
Defined.

Definition Quotient_ind_beta_qglue@{i j k l}
{A : Type@{i}} (R : Relation@{i j} A)
(P : Quotient@{i j k} R Type@{l}) {sP : x, IsHSet (P x)}
(pclass : x, P (class_of R x))
(peq : x y (H : R x y), qglue H # pclass x = pclass y)
(x y : A) (p : R x y)
: apD (Quotient_ind@{i j k l} R P pclass peq) (qglue p) = peq x y p.
Proof.
refine (apD_compose' tr _ _ @ _).
refine (ap _ (Coeq_ind_beta_cglue _ _ _ _) @ _).
apply concat_V_pp.
Defined.

Definition Quotient_rec@{i j k l}
{A : Type@{i}} (R : Relation@{i j} A)
(P : Type@{l}) `{IsHSet P} (pclass : A P)
(peq : x y, R x y pclass x = pclass y)
: Quotient@{i j k} R P.
Proof.
eapply Trunc_rec, Coeq_rec.
intros [a [b p]].
by apply peq.
Defined.

Definition Quotient_rec_beta_qglue @{i j k l}
{A : Type@{i}} (R : Relation@{i j} A)
(P : Type@{l}) `{IsHSet P} (pclass : A P)
(peq : x y, R x y pclass x = pclass y)
(x y : A) (p : R x y)
: ap (Quotient_rec@{i j k l} R P pclass peq) (qglue p) = peq x y p.
Proof.
refine ((ap_compose tr _ _)^ @ _).
srapply Coeq_rec_beta_cglue.
Defined.

Arguments Quotient : simpl never.
Arguments class_of : simpl never.
Arguments qglue : simpl never.
Arguments Quotient_ind_beta_qglue : simpl never.
Arguments Quotient_rec_beta_qglue : simpl never.

Notation "A / R" := (Quotient (A:=A) R).

Section Equiv.

Context `{Univalence} {A : Type} (R : Relation A) `{is_mere_relation _ R}
`{Transitive _ R} `{Symmetric _ R} `{Reflexive _ R}.

Definition in_class : A / R A hProp.
Proof.
srapply Quotient_ind.
{ intros a b.
exact (BuildhProp (R a b)). }
intros x y p.
refine (transport_const _ _ @ _).
funext z.
apply path_hprop.
srapply equiv_iff_hprop; cbn.
1: apply (transitivity (symmetry _ _ p)).
apply (transitivity p).
Defined.

Definition Quotient_ind_hprop
(P : A / R Type) `{ x, IsHProp (P x)}
(dclass : x, P (class_of R x)) : q, P q.
Proof.
srapply (Quotient_ind R P dclass).
all: try (intro; apply trunc_succ).
intros x y p.
apply path_ishprop.
Defined.

Global Instance decidable_in_class `{ x y, Decidable (R x y)}
: x a, Decidable (in_class x a).
Proof.
by srapply Quotient_ind_hprop.
Defined.

Lemma path_in_class_of : q x, in_class q x q = class_of R x.
Proof.
srapply Quotient_ind.
{ intros x y p.
apply (qglue p). }
intros x y p.
funext ? ?.
apply hset_path2.
Defined.

Lemma related_quotient_paths : x y,
class_of R x = class_of R y R x y.
Proof.
intros x y p.
change (in_class (class_of R x) y).
destruct p^.
cbv; reflexivity.
Defined.

Thm 10.1.8
Theorem path_quotient : x y,
R x y <~> (class_of R x = class_of R y).
Proof.
intros ??.
apply equiv_iff_hprop.
- apply qglue.
- apply related_quotient_paths.
Defined.

Definition Quotient_rec2 `{Funext} {B : hSet} {dclass : A A B}
{dequiv : x x', R x x' y y',
R y y' dclass x y = dclass x' y'}
: A / R A / R B.
Proof.
srapply Quotient_rec.
{ intro a.
srapply Quotient_rec.
{ revert a.
assumption. }
by apply (dequiv a a). }
intros x y p.
apply path_forall.
srapply Quotient_ind.
{ cbn; intro a.
by apply dequiv. }
intros a b q.
apply path_ishprop.
Defined.

Definition Quotient_ind_hprop' (P : A / R Type)
`{ x, IsHProp (P (class_of _ x))}
(dclass : x, P (class_of _ x)) : y, P y.
Proof.
apply Quotient_ind with dclass.
{ srapply Quotient_ind.
1: intro; apply trunc_succ.
intros ???; apply path_ishprop. }
intros; apply path_ishprop.
Defined.

The map class_of : A -> A/R is a surjection.
Global Instance issurj_class_of : IsSurjection (class_of R).
Proof.
apply BuildIsSurjection.
srapply Quotient_ind_hprop.
intro x.
apply tr.
by x.
Defined.

Theorem equiv_quotient_ump (B : hSet)
: (A / R B) <~> {f : A B & x y, R x y f x = f y}.
Proof.
+ intro f.
(compose f (class_of R)).
intros; f_ap.
by apply qglue.
+ intros [f H'].
apply (Quotient_rec _ _ _ H').
+ intros [f Hf].
by apply equiv_path_sigma_hprop.
+ intros f.
apply path_forall.
srapply Quotient_ind_hprop.
reflexivity.
Defined.

TODO: The equivalence with VVquotient A//R. 10.1.10. Equivalence Relations are effective and there is an equivalence A/R<~>A//R.
This will need propositional resizing if we don't want to raise the universe level.
The theory of canonical quotients is developed by C.Cohen: http://perso.crans.org/cohen/work/quotients/

End Equiv.

Section Functoriality.

Definition Quotient_functor
{A : Type} (R : Relation A)
{B : Type} (S : Relation B)
(f : A B) (fresp : x y, R x y S (f x) (f y))
: Quotient R Quotient S.
Proof.
refine (Quotient_rec R _ (class_of S o f) _).
intros x y r.
apply qglue, fresp, r.
Defined.

Definition Quotient_functor_idmap
{A : Type} {R : Relation A}
: Quotient_functor R R idmap (fun x yidmap) == idmap.
Proof.
by srapply Quotient_ind_hprop.
Defined.

Definition Quotient_functor_compose
{A : Type} {R : Relation A}
{B : Type} {S : Relation B}
{C : Type} {T : Relation C}
(f : A B) (fresp : x y, R x y S (f x) (f y))
(g : B C) (gresp : x y, S x y T (g x) (g y))
: Quotient_functor R T (g o f) (fun x y(gresp _ _) o (fresp x y))
== Quotient_functor S T g gresp o Quotient_functor R S f fresp.
Proof.
by srapply Quotient_ind_hprop.
Defined.

Context {A : Type} (R : Relation A)
{B : Type} (S : Relation B).

Global Instance isequiv_quotient_functor (f : A B)
(fresp : x y, R x y S (f x) (f y)) `{IsEquiv _ _ f}
: IsEquiv (Quotient_functor R S f (fun x yfst (fresp x y))).
Proof.
srapply (isequiv_adjointify _ (Quotient_functor S R f^-1 _)).
{ intros u v s.
apply (snd (fresp _ _)).
abstract (do 2 rewrite eisretr; apply s). }
all: srapply Quotient_ind.
+ intros b; simpl.
apply ap, eisretr.
+ intros; apply path_ishprop.
+ intros a; simpl.
apply ap, eissect.
+ intros; apply path_ishprop.
Defined.

Definition equiv_quotient_functor (f : A B) `{IsEquiv _ _ f}
(fresp : x y, R x y S (f x) (f y))
: Quotient R <~> Quotient S
:= Build_Equiv _ _ (Quotient_functor R S f (fun x yfst (fresp x y))) _.

Definition equiv_quotient_functor' (f : A <~> B)
(fresp : x y, R x y S (f x) (f y))
: Quotient R <~> Quotient S
:= equiv_quotient_functor f fresp.

End Functoriality.

Section Kernel.

## Quotients of kernels of maps to sets give a surjection/mono factorization.

Context `{Funext}.
Universe i.

A function we want to factor.
Context {A : Type@{i}} {B : Type} `{IsHSet B} (f : A B).

A mere Relation equivalent to its kernel.
Context (R : Relation A)
(is_ker : x y, f x = f y <~> R x y).

Theorem quotient_kernel_factor
: (C : Type@{i}) (e : A C) (m : C B),
IsHSet C × IsSurjection e × IsEmbedding m × (f = m o e).
Proof.
(Quotient R).
(class_of R).
srefine (_;_).
{ apply Quotient_ind with f; try exact _.
intros x y p.
transitivity (f x).
- apply transport_const.
- exact ((is_ker x y)^-1 p). }
repeat split; try exact _.
intro u.
apply hprop_allpath.
intros [x q] [y p'].
apply path_sigma_hprop; simpl.
revert x y q p'.
srapply Quotient_ind.
2: intros; apply path_ishprop.
intro a.
srapply Quotient_ind.
2: intros; apply path_ishprop.
intros a' p p'.
apply qglue, is_ker.
exact (p @ p'^).
Defined.

End Kernel.