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.
    srapply equiv_adjointify.
    + 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.