Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.
Require Import HSet.
Require Import TruncType.
Require Import Colimits.GraphQuotient.
Require Import Truncations.Core.
Require Import PropResizing.

Local Open Scope path_scope.

(** * The set-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 0-truncated graph quotient. *)

Definition Quotient@{i j k} {A : Type@{i}} (R : Relation@{i j} A) : Type@{k}
  := Trunc@{k} 0 (GraphQuotient@{i j k} R).

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

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 p => ap tr (gqglue 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 : forall x, IsHSet (P x)}
  (pclass : forall x, P (class_of R x))
  (peq : forall x y (H : R x y), qglue H # pclass x = pclass y)
  : forall q, P q.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
forall q : Quotient R, P q
Proof.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
forall q : Quotient R, P q
  eapply Trunc_ind, GraphQuotient_ind.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
forall aa : Trunc 0 (GraphQuotient R), IsHSet (P aa)
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
forall (a b : A) (s : R a b),
transport (fun x : GraphQuotient R => P (tr x))
  (gqglue s) (?gq' a) = 
?gq' b
  1: assumption.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
forall (a b : A) (s : R a b),
transport (fun x : GraphQuotient R => P (tr x))
  (gqglue s) (?gq' a) = ?gq' b
  intros a b p.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
a, b: A
p: R a b
transport (fun x : GraphQuotient R => P (tr x))
  (gqglue p) (?gq' a) = ?gq' b
  refine (transport_compose _ _ _ _ @ _).
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
a, b: A
p: R a b
transport P (ap tr (gqglue p)) (?gq' a) = ?gq' b
  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 : forall x, IsHSet (P x)}
  (pclass : forall x, P (class_of R x))
  (peq : forall 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.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
x, y: A
p: R x y
apD (Quotient_ind R P pclass peq) (qglue p) =
peq x y p
Proof.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
x, y: A
p: R x y
apD (Quotient_ind R P pclass peq) (qglue p) =
peq x y p
  refine (apD_compose' tr _ _ @ _).
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
x, y: A
p: R x y
(transport_compose P tr (gqglue p)
   (Quotient_ind R P pclass peq (tr (gq x))))^ @
apD
  (fun x : GraphQuotient R =>
   Quotient_ind R P pclass peq (tr x)) (gqglue p) =
peq x y p
  unfold Quotient_ind.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
x, y: A
p: R x y
(transport_compose P tr (gqglue p)
   (Trunc_ind P
      (GraphQuotient_ind
         (fun x : GraphQuotient R => P (tr x))
         (fun a : A => pclass a)
         (fun (a b : A) (p : R a b) =>
          transport_compose P tr (gqglue p) (pclass a) @
          peq a b p)) (tr (gq x))))^ @
apD
  (fun x : GraphQuotient R =>
   Trunc_ind P
     (GraphQuotient_ind
        (fun x0 : GraphQuotient R => P (tr x0))
        (fun a : A => pclass a)
        (fun (a b : A) (p : R a b) =>
         transport_compose P tr (gqglue p) (pclass a) @
         peq a b p)) (tr x)) (gqglue p) = peq x y p
  refine (ap _ (GraphQuotient_ind_beta_gqglue _ pclass
    (fun a b p0 => transport_compose P tr _ _ @ peq a b p0) _ _ _) @ _).
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall x : A, P (class_of R x)
peq: forall (x y : A) (H : R x y),
transport P (qglue H) (pclass x) = pclass y
x, y: A
p: R x y
(transport_compose P tr (gqglue p)
   (Trunc_ind P
      (GraphQuotient_ind
         (fun x : GraphQuotient R => P (tr x))
         (fun a : A => pclass a)
         (fun (a b : A) (p : R a b) =>
          transport_compose P tr (gqglue p) (pclass a) @
          peq a b p)) (tr (gq x))))^ @
(transport_compose P tr (gqglue p) (pclass x) @
 peq x y p) = peq x y p
  rapply 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 : forall x y, R x y -> pclass x = pclass y)
  : Quotient@{i j k} R -> P.
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall x y : A, R x y -> pclass x = pclass y
Quotient R -> P
Proof.
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall x y : A, R x y -> pclass x = pclass y
Quotient R -> P
  eapply Trunc_rec, GraphQuotient_rec.
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall x y : A, R x y -> pclass x = pclass y
forall a b : A, R a b -> ?c a = ?c b
  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 : forall 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.
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall x y : A, R x y -> pclass x = pclass y
x, y: A
p: R x y
ap (Quotient_rec R P pclass peq) (qglue p) = peq x y p
Proof.
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall x y : A, R x y -> pclass x = pclass y
x, y: A
p: R x y
ap (Quotient_rec R P pclass peq) (qglue p) = peq x y p
  refine ((ap_compose tr _ _)^ @ _).
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall x y : A, R x y -> pclass x = pclass y
x, y: A
p: R x y
ap
  (fun x : GraphQuotient R =>
   Quotient_rec R P pclass peq (tr x)) (gqglue p) =
peq x y p
  srapply GraphQuotient_rec_beta_gqglue.
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}.

  (* The proposition of being in a given class in a quotient. *)
  Definition in_class : A / R -> A -> HProp.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
A / R -> A -> HProp
  Proof.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
A / R -> A -> HProp
    srapply Quotient_ind.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall x : A,
(fun _ : A / R => A -> HProp) (class_of R x)
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall (x y : A) (H3 : R x y),
transport (fun _ : A / R => A -> HProp) 
  (qglue H3) (?pclass x) = 
?pclass y
    {
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall x : A,
(fun _ : A / R => A -> HProp) (class_of R x) intros a b.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
a, b: A
HProp
      exact (Build_HProp (R a b)). }
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall (x y : A) (H : R x y),
transport (fun _ : A / R => A -> HProp) (qglue H)
  ((fun a : A =>
    (fun b : A => Build_HProp (R a b))
    :
    (fun _ : A / R => A -> HProp) (class_of R a)) x) =
(fun a : A =>
 (fun b : A => Build_HProp (R a b))
 :
 (fun _ : A / R => A -> HProp) (class_of R a)) y
    intros x y p.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: R x y
transport (fun _ : A / R => A -> HProp) (qglue p)
  ((fun a : A =>
    (fun b : A => Build_HProp (R a b))
    :
    (fun _ : A / R => A -> HProp) (class_of R a)) x) =
(fun a : A =>
 (fun b : A => Build_HProp (R a b))
 :
 (fun _ : A / R => A -> HProp) (class_of R a)) y
    refine (transport_const _ _ @ _).
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: R x y
(fun b : A => Build_HProp (R x b)) =
(fun b : A => Build_HProp (R y b))
    funext z.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: R x y
z: A
Build_HProp (R x z) = Build_HProp (R y z)
    apply path_hprop.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: R x y
z: A
Build_HProp (R x z) <~> Build_HProp (R y z)
    srapply equiv_iff_hprop; cbn.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: R x y
z: A
R x z -> R y z
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: R x y
z: A
R y z -> R x z
    1: apply (transitivity (symmetry _ _ p)).
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: R x y
z: A
R y z -> R x z
    apply (transitivity p).
  Defined.

  (* Quotient induction into a hprop. *)
  Definition Quotient_ind_hprop
    (P : A / R -> Type) `{forall x, IsHProp (P x)}
    (dclass : forall x, P (class_of R x)) : forall q, P q.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A / R, IsHProp (P x)
dclass: forall x : A, P (class_of R x)
forall q : A / R, P q
  Proof.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A / R, IsHProp (P x)
dclass: forall x : A, P (class_of R x)
forall q : A / R, P q
    srapply (Quotient_ind R P dclass).
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A / R, IsHProp (P x)
dclass: forall x : A, P (class_of R x)
forall (x y : A) (H : R x y),
transport P (qglue H) (dclass x) = dclass y
    all: try (intro; apply trunc_succ).
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A / R, IsHProp (P x)
dclass: forall x : A, P (class_of R x)
forall (x y : A) (H : R x y),
transport P (qglue H) (dclass x) = dclass y
    intros x y p.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A / R, IsHProp (P x)
dclass: forall x : A, P (class_of R x)
x, y: A
p: R x y
transport P (qglue p) (dclass x) = dclass y
    apply path_ishprop.
  Defined.

  (* Being in a class is decidable if the Relation is decidable. *)
  Global Instance decidable_in_class `{forall x y, Decidable (R x y)}
  : forall x a, Decidable (in_class x a).
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: forall x y : A, Decidable (R x y)
forall (x : A / R) (a : A), Decidable (in_class x a)
  Proof.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: forall x y : A, Decidable (R x y)
forall (x : A / R) (a : A), Decidable (in_class x a)
    by srapply Quotient_ind_hprop.
  Defined.

  (* if x is in a class q, then the class of x is equal to q. *)
  Lemma path_in_class_of : forall q x, in_class q x -> q = class_of R x.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall (q : A / R) (x : A),
in_class q x -> q = class_of R x
  Proof.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall (q : A / R) (x : A),
in_class q x -> q = class_of R x
    srapply Quotient_ind.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall x : A,
(fun q : A / R =>
 forall x0 : A, in_class q x0 -> q = class_of R x0)
  (class_of R x)
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall (x y : A) (H3 : R x y),
transport
  (fun q : A / R =>
   forall x0 : A, in_class q x0 -> q = class_of R x0)
  (qglue H3) (?pclass x) = 
?pclass y
    {
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall x : A,
(fun q : A / R =>
 forall x0 : A, in_class q x0 -> q = class_of R x0)
  (class_of R x) intros x y p.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: in_class (class_of R x) y
class_of R x = class_of R y
      apply (qglue p). }
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall (x y : A) (H : R x y),
transport
  (fun q : A / R =>
   forall x0 : A, in_class q x0 -> q = class_of R x0)
  (qglue H)
  ((fun x0 : A =>
    (fun (y0 : A) (p : in_class (class_of R x0) y0) =>
     qglue p)
    :
    (fun q : A / R =>
     forall x1 : A, in_class q x1 -> q = class_of R x1)
      (class_of R x0)) x) =
(fun x0 : A =>
 (fun (y0 : A) (p : in_class (class_of R x0) y0) =>
  qglue p)
 :
 (fun q : A / R =>
  forall x1 : A, in_class q x1 -> q = class_of R x1)
   (class_of R x0)) y
    intros x y p.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: R x y
transport
  (fun q : A / R =>
   forall x : A, in_class q x -> q = class_of R x)
  (qglue p)
  ((fun x : A =>
    (fun (y : A) (p : in_class (class_of R x) y) =>
     qglue p)
    :
    (fun q : A / R =>
     forall x0 : A, in_class q x0 -> q = class_of R x0)
      (class_of R x)) x) =
(fun x : A =>
 (fun (y : A) (p : in_class (class_of R x) y) =>
  qglue p)
 :
 (fun q : A / R =>
  forall x0 : A, in_class q x0 -> q = class_of R x0)
   (class_of R x)) y
    funext ? ?.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: R x y
x0: A
x1: in_class (class_of R y) x0
transport
  (fun q : A / R =>
   forall x : A, in_class q x -> q = class_of R x)
  (qglue p)
  (fun (y : A) (p : in_class (class_of R x) y) =>
   qglue p) x0 x1 = qglue x1
    apply hset_path2.
  Defined.

  Lemma related_quotient_paths : forall x y,
    class_of R x = class_of R y -> R x y.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall x y : A, class_of R x = class_of R y -> R x y
  Proof.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall x y : A, class_of R x = class_of R y -> R x y
    intros x y p.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: class_of R x = class_of R y
R x y
    change (in_class (class_of R x) y).
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: class_of R x = class_of R y
in_class (class_of R x) y
    destruct p^.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
p: class_of R y = class_of R y
in_class (class_of R y) y
    cbv; reflexivity.
  Defined.

  (** Thm 10.1.8 *)
  Theorem path_quotient : forall x y,
    R x y <~> (class_of R x = class_of R y).
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall x y : A, R x y <~> class_of R x = class_of R y
  Proof.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall x y : A, R x y <~> class_of R x = class_of R y
    intros ??.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
R x y <~> class_of R x = class_of R y
    apply equiv_iff_hprop.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
R x y -> class_of R x = class_of R y
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
class_of R x = class_of R y -> R x y
    -
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
R x y -> class_of R x = class_of R y apply qglue.
    -
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x, y: A
class_of R x = class_of R y -> R x y apply related_quotient_paths.
  Defined.

  Definition Quotient_rec2 `{Funext} {B : HSet} {dclass : A -> A -> B}
    {dequiv : forall x x', R x x' -> forall y y',
      R y y' -> dclass x y = dclass x' y'}
    : A / R -> A / R -> B.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
A / R -> A / R -> B
  Proof.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
A / R -> A / R -> B
    srapply Quotient_rec.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
A -> A / R -> B
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
forall x y : A, R x y -> ?pclass x = ?pclass y
    {
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
A -> A / R -> B intro a.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
a: A
A / R -> B
      srapply Quotient_rec.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
a: A
A -> B
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
a: A
forall x y : A, R x y -> ?pclass x = ?pclass y
      {
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
a: A
A -> B revert a.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
A -> A -> B
        assumption. }
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
a: A
forall x y : A, R x y -> dclass a x = dclass a y
      by apply (dequiv a a). }
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
forall x y : A,
R x y ->
(fun a : A =>
 Quotient_rec R B (dclass a) (dequiv a a (H2 a))) x =
(fun a : A =>
 Quotient_rec R B (dclass a) (dequiv a a (H2 a))) y
    intros x y p.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
x, y: A
p: R x y
(fun a : A =>
 Quotient_rec R B (dclass a) (dequiv a a (H2 a))) x =
(fun a : A =>
 Quotient_rec R B (dclass a) (dequiv a a (H2 a))) y
    apply path_forall.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
x, y: A
p: R x y
Quotient_rec R B (dclass x) (dequiv x x (H2 x)) ==
Quotient_rec R B (dclass y) (dequiv y y (H2 y))
    srapply Quotient_ind.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
x, y: A
p: R x y
forall x0 : A,
(fun q : A / R =>
 Quotient_rec R B (dclass x) (dequiv x x (H2 x)) q =
 Quotient_rec R B (dclass y) (dequiv y y (H2 y)) q)
  (class_of R x0)
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
x, y: A
p: R x y
forall (x0 y0 : A) 
(H4 : R x0 y0),
transport
  (fun q : A / R =>
   Quotient_rec R B (dclass x) (dequiv x x (H2 x)) q =
   Quotient_rec R B (dclass y) (dequiv y y (H2 y)) q)
  (qglue H4) (?pclass x0) = 
?pclass y0
    {
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
x, y: A
p: R x y
forall x0 : A,
(fun q : A / R =>
 Quotient_rec R B (dclass x) (dequiv x x (H2 x)) q =
 Quotient_rec R B (dclass y) (dequiv y y (H2 y)) q)
  (class_of R x0) cbn; intro a.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
x, y: A
p: R x y
a: A
Quotient_rec R B (dclass x) (dequiv x x (H2 x))
  (class_of R a) =
Quotient_rec R B (dclass y) (dequiv y y (H2 y))
  (class_of R a)
      by apply dequiv. }
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
x, y: A
p: R x y
forall (x0 y0 : A) (H : R x0 y0),
transport
  (fun q : A / R =>
   Quotient_rec R B (dclass x) (dequiv x x (H2 x)) q =
   Quotient_rec R B (dclass y) (dequiv y y (H2 y)) q)
  (qglue H)
  (((fun a : A => dequiv x y p a a (H2 a))
    :
    forall x1 : A,
    (fun q : A / R =>
     Quotient_rec R B (dclass x) (dequiv x x (H2 x)) q =
     Quotient_rec R B (dclass y) (dequiv y y (H2 y)) q)
      (class_of R x1)) x0) =
((fun a : A => dequiv x y p a a (H2 a))
 :
 forall x1 : A,
 (fun q : A / R =>
  Quotient_rec R B (dclass x) (dequiv x x (H2 x)) q =
  Quotient_rec R B (dclass y) (dequiv y y (H2 y)) q)
   (class_of R x1)) y0
    intros a b q.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
H3: Funext
B: HSet
dclass: A -> A -> B
dequiv: forall x x' : A,
R x x' ->
forall y y' : A,
R y y' -> dclass x y = dclass x' y'
x, y: A
p: R x y
a, b: A
q: R a b
transport
  (fun q : A / R =>
   Quotient_rec R B (dclass x) (dequiv x x (H2 x)) q =
   Quotient_rec R B (dclass y) (dequiv y y (H2 y)) q)
  (qglue q)
  (((fun a : A => dequiv x y p a a (H2 a))
    :
    forall x0 : A,
    (fun q : A / R =>
     Quotient_rec R B (dclass x) (dequiv x x (H2 x)) q =
     Quotient_rec R B (dclass y) (dequiv y y (H2 y)) q)
      (class_of R x0)) a) =
((fun a : A => dequiv x y p a a (H2 a))
 :
 forall x0 : A,
 (fun q : A / R =>
  Quotient_rec R B (dclass x) (dequiv x x (H2 x)) q =
  Quotient_rec R B (dclass y) (dequiv y y (H2 y)) q)
   (class_of R x0)) b
    apply path_ishprop.
  Defined.

  Definition Quotient_ind_hprop' (P : A / R -> Type)
    `{forall x, IsHProp (P (class_of _ x))}
    (dclass : forall x, P (class_of _ x)) : forall y, P y.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall y : A / R, P y
  Proof.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall y : A / R, P y
    apply Quotient_ind with dclass.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall x : A / R, IsHSet (P x)
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall (x y : A) (H : R x y),
transport P (qglue H) (dclass x) = dclass y
    {
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall x : A / R, IsHSet (P x) srapply Quotient_ind.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall x : A,
(fun q : A / R => IsHSet (P q)) (class_of R x)
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall (x y : A) (H4 : R x y),
transport (fun q : A / R => IsHSet (P q)) 
  (qglue H4) (?pclass x) = 
?pclass y
      1: intro; apply istrunc_succ.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall (x y : A) (H : R x y),
transport (fun q : A / R => IsHSet (P q)) (qglue H)
  ((fun x0 : A => istrunc_succ) x) =
(fun x0 : A => istrunc_succ) y
      intros ???; apply path_ishprop. }
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
P: A / R -> Type
H3: forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall (x y : A) (H : R x y),
transport P (qglue H) (dclass x) = dclass y
    intros; apply path_ishprop.
  Defined.

  (** The map class_of : A -> A/R is a surjection. *)
  Global Instance issurj_class_of : IsSurjection (class_of R).
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
ReflectiveSubuniverse.IsConnMap (Tr (-1)) (class_of R)
  Proof.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
ReflectiveSubuniverse.IsConnMap (Tr (-1)) (class_of R)
    apply BuildIsSurjection.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall b : A / R, merely (hfiber (class_of R) b)
    srapply Quotient_ind_hprop.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
forall x : A,
(fun q : A / R =>
 trunctype_type (merely (hfiber (class_of R) q)))
  (class_of R x)
    intro x.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x: A
(fun q : A / R =>
 trunctype_type (merely (hfiber (class_of R) q)))
  (class_of R x)
    apply tr.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
x: A
hfiber (class_of R) (class_of R x)
    by exists x.
  Defined.

  (* Universal property of quotient *)
  (* Lemma 6.10.3 *)
  Theorem equiv_quotient_ump (B : HSet)
    : (A / R -> B) <~> {f : A -> B & forall x y, R x y -> f x = f y}.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
(A / R -> B) <~>
{f : A -> B & forall x y : A, R x y -> f x = f y}
  Proof.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
(A / R -> B) <~>
{f : A -> B & forall x y : A, R x y -> f x = f y}
    srapply equiv_adjointify.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
(A / R -> B) ->
{f : A -> B & forall x y : A, R x y -> f x = f y}
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
{f : A -> B & forall x y : A, R x y -> f x = f y} ->
A / R -> B
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
?f o ?g == idmap
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
?g o ?f == idmap
    +
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
(A / R -> B) ->
{f : A -> B & forall x y : A, R x y -> f x = f y} intro f.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
f: A / R -> B
{f : A -> B & forall x y : A, R x y -> f x = f y}
      exists (compose f (class_of R)).
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
f: A / R -> B
forall x y : A,
R x y -> f (class_of R x) = f (class_of R y)
      intros; f_ap.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
f: A / R -> B
x, y: A
X: R x y
class_of R x = class_of R y
      by apply qglue.
    +
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
{f : A -> B & forall x y : A, R x y -> f x = f y} ->
A / R -> B intros [f H'].
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
f: A -> B
H': forall x y : A, R x y -> f x = f y
A / R -> B
      apply (Quotient_rec _ _ _ H').
    +
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
(fun f : A / R -> B =>
 (fun x : A => f (class_of R x);
 fun (x y : A) (H : R x y) => ap11 1 (qglue H)))
o (fun
     X : {f : A -> B &
         forall x y : A, R x y -> f x = f y} =>
   (fun (f : A -> B)
      (H' : forall x y : A, R x y -> f x = f y) =>
    Quotient_rec R B f H') X.1 X.2) == idmap intros [f Hf].
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
f: A -> B
Hf: forall x y : A, R x y -> f x = f y
(fun x : A => Quotient_rec R B f Hf (class_of R x);
fun (x y : A) (H : R x y) => ap11 1 (qglue H)) =
(f; Hf)
      by apply equiv_path_sigma_hprop.
    +
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
(fun
   X : {f : A -> B &
       forall x y : A, R x y -> f x = f y} =>
 (fun (f : A -> B)
    (H' : forall x y : A, R x y -> f x = f y) =>
  Quotient_rec R B f H') X.1 X.2)
o (fun f : A / R -> B =>
   (fun x : A => f (class_of R x);
   fun (x y : A) (H : R x y) => ap11 1 (qglue H))) ==
idmap intros f.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
f: A / R -> B
Quotient_rec R B (fun x : A => f (class_of R x))
  (fun (x y : A) (H : R x y) => ap11 1 (qglue H)) = f
      apply path_forall.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
f: A / R -> B
Quotient_rec R B (fun x : A => f (class_of R x))
  (fun (x y : A) (H : R x y) => ap11 1 (qglue H)) == f
      srapply Quotient_ind_hprop.
H: Univalence
A: Type
R: Relation A
is_mere_relation0: is_mere_relation A R
H0: Transitive R
H1: Symmetric R
H2: Reflexive R
B: HSet
f: A / R -> B
forall x : A,
(fun q : A / R =>
 Quotient_rec R B (fun x0 : A => f (class_of R x0))
   (fun (x0 y : A) (H : R x0 y) => ap11 1 (qglue H)) q =
 f q) (class_of R x)
      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.

  (* TODO: Develop a notion of set with Relation and use that instead of manually adding Relation preserving conditions. *)

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

  Definition Quotient_functor_idmap
    {A : Type} {R : Relation A}
    : Quotient_functor R R idmap (fun x y => idmap) == idmap.
A: Type
R: Relation A
Quotient_functor R R idmap (fun x y : A => idmap) ==
idmap
  Proof.
A: Type
R: Relation A
Quotient_functor R R idmap (fun x y : A => idmap) ==
idmap
    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 : forall x y, R x y -> S (f x) (f y))
    (g : B -> C) (gresp : forall 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.
A: Type
R: Relation A
B: Type
S: Relation B
C: Type
T: Relation C
f: A -> B
fresp: forall x y : A, R x y -> S (f x) (f y)
g: B -> C
gresp: forall x y : B, S x y -> T (g x) (g y)
Quotient_functor R T (g o f)
  (fun x y : A => gresp (f x) (f y) o fresp x y) ==
Quotient_functor S T g gresp
o Quotient_functor R S f fresp
  Proof.
A: Type
R: Relation A
B: Type
S: Relation B
C: Type
T: Relation C
f: A -> B
fresp: forall x y : A, R x y -> S (f x) (f y)
g: B -> C
gresp: forall x y : B, S x y -> T (g x) (g y)
Quotient_functor R T (g o f)
  (fun x y : A => gresp (f x) (f y) o fresp x y) ==
Quotient_functor S T g gresp
o Quotient_functor R S f fresp
    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 : forall x y, R x y <-> S (f x) (f y)) `{IsEquiv _ _ f}
    : IsEquiv (Quotient_functor R S f (fun x y => fst (fresp x y))).
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
IsEquiv
  (Quotient_functor R S f
     (fun x y : A => fst (fresp x y)))
  Proof.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
IsEquiv
  (Quotient_functor R S f
     (fun x y : A => fst (fresp x y)))
    srapply (isequiv_adjointify _ (Quotient_functor S R f^-1 _)).
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall x y : B, S x y -> R (f^-1 x) (f^-1 y)
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
Quotient_functor R S f
  (fun x y : A => fst (fresp x y))
o Quotient_functor S R f^-1 ?fresp == idmap
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
Quotient_functor S R f^-1 ?fresp
o Quotient_functor R S f
    (fun x y : A => fst (fresp x y)) == idmap
    {
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall x y : B, S x y -> R (f^-1 x) (f^-1 y) intros u v s.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
u, v: B
s: S u v
R (f^-1 u) (f^-1 v)
      apply (snd (fresp _ _)).
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
u, v: B
s: S u v
S (f (f^-1 u)) (f (f^-1 v))
      abstract (do 2 rewrite eisretr; apply s). }
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
Quotient_functor R S f
  (fun x y : A => fst (fresp x y))
o Quotient_functor S R f^-1
    (fun (u v : B) (s : S u v) =>
     snd (fresp (f^-1 u) (f^-1 v))
       (isequiv_quotient_functor_subproof f H u v s)) ==
idmap
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
Quotient_functor S R f^-1
  (fun (u v : B) (s : S u v) =>
   snd (fresp (f^-1 u) (f^-1 v))
     (isequiv_quotient_functor_subproof f H u v s))
o Quotient_functor R S f
    (fun x y : A => fst (fresp x y)) == idmap
    all: srapply Quotient_ind.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall x : B,
(fun q : B / S =>
 (Quotient_functor R S f
    (fun x0 y : A => fst (fresp x0 y))
  o Quotient_functor S R f^-1
      (fun (u v : B) (s : S u v) =>
       snd (fresp (f^-1 u) (f^-1 v))
         (isequiv_quotient_functor_subproof f H u v s)))
   q = idmap q) (class_of S x)
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall (x y : B) (H0 : S x y),
transport
  (fun q : B / S =>
   (Quotient_functor R S f
      (fun x0 y0 : A => fst (fresp x0 y0))
    o Quotient_functor S R f^-1
        (fun (u v : B) (s : S u v) =>
         snd (fresp (f^-1 u) (f^-1 v))
           (isequiv_quotient_functor_subproof f H u v
              s))) q = idmap q) 
  (qglue H0) (?pclass x) = 
?pclass y
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall x : A,
(fun q : A / R =>
 (Quotient_functor S R f^-1
    (fun (u v : B) (s : S u v) =>
     snd (fresp (f^-1 u) (f^-1 v))
       (isequiv_quotient_functor_subproof f H u v s))
  o Quotient_functor R S f
      (fun x0 y : A => fst (fresp x0 y))) q = 
 idmap q) (class_of R x)
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall (x y : A) (H0 : R x y),
transport
  (fun q : A / R =>
   (Quotient_functor S R f^-1
      (fun (u v : B) (s : S u v) =>
       snd (fresp (f^-1 u) (f^-1 v))
         (isequiv_quotient_functor_subproof f H u v s))
    o Quotient_functor R S f
        (fun x0 y0 : A => fst (fresp x0 y0))) q =
   idmap q) (qglue H0) (?pclass0 x) = 
?pclass0 y
    +
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall x : B,
(fun q : B / S =>
 (Quotient_functor R S f
    (fun x0 y : A => fst (fresp x0 y))
  o Quotient_functor S R f^-1
      (fun (u v : B) (s : S u v) =>
       snd (fresp (f^-1 u) (f^-1 v))
         (isequiv_quotient_functor_subproof f H u v s)))
   q = idmap q) (class_of S x) intros b; simpl.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
b: B
class_of S (f (f^-1 b)) = class_of S b
      apply ap, eisretr.
    +
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall (x y : B) (H0 : S x y),
transport
  (fun q : B / S =>
   (Quotient_functor R S f
      (fun x0 y0 : A => fst (fresp x0 y0))
    o Quotient_functor S R f^-1
        (fun (u v : B) (s : S u v) =>
         snd (fresp (f^-1 u) (f^-1 v))
           (isequiv_quotient_functor_subproof f H u v
              s))) q = idmap q) (qglue H0)
  ((fun b : B =>
    ap (class_of S) (eisretr f b)
    :
    (fun q : B / S =>
     (Quotient_functor R S f
        (fun x0 y0 : A => fst (fresp x0 y0))
      o Quotient_functor S R f^-1
          (fun (u v : B) (s : S u v) =>
           snd (fresp (f^-1 u) (f^-1 v))
             (isequiv_quotient_functor_subproof f H u
                v s))) q = idmap q) (class_of S b)) x) =
(fun b : B =>
 ap (class_of S) (eisretr f b)
 :
 (fun q : B / S =>
  (Quotient_functor R S f
     (fun x0 y0 : A => fst (fresp x0 y0))
   o Quotient_functor S R f^-1
       (fun (u v : B) (s : S u v) =>
        snd (fresp (f^-1 u) (f^-1 v))
          (isequiv_quotient_functor_subproof f H u v s)))
    q = idmap q) (class_of S b)) y intros; apply path_ishprop.
    +
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall x : A,
(fun q : A / R =>
 (Quotient_functor S R f^-1
    (fun (u v : B) (s : S u v) =>
     snd (fresp (f^-1 u) (f^-1 v))
       (isequiv_quotient_functor_subproof f H u v s))
  o Quotient_functor R S f
      (fun x0 y : A => fst (fresp x0 y))) q = idmap q)
  (class_of R x) intros a; simpl.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
a: A
class_of R (f^-1 (f a)) = class_of R a
      apply ap, eissect.
    +
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall (x y : A) (H0 : R x y),
transport
  (fun q : A / R =>
   (Quotient_functor S R f^-1
      (fun (u v : B) (s : S u v) =>
       snd (fresp (f^-1 u) (f^-1 v))
         (isequiv_quotient_functor_subproof f H u v s))
    o Quotient_functor R S f
        (fun x0 y0 : A => fst (fresp x0 y0))) q =
   idmap q) (qglue H0)
  ((fun a : A =>
    ap (class_of R) (eissect f a)
    :
    (fun q : A / R =>
     (Quotient_functor S R f^-1
        (fun (u v : B) (s : S u v) =>
         snd (fresp (f^-1 u) (f^-1 v))
           (isequiv_quotient_functor_subproof f H u v
              s))
      o Quotient_functor R S f
          (fun x0 y0 : A => fst (fresp x0 y0))) q =
     idmap q) (class_of R a)) x) =
(fun a : A =>
 ap (class_of R) (eissect f a)
 :
 (fun q : A / R =>
  (Quotient_functor S R f^-1
     (fun (u v : B) (s : S u v) =>
      snd (fresp (f^-1 u) (f^-1 v))
        (isequiv_quotient_functor_subproof f H u v s))
   o Quotient_functor R S f
       (fun x0 y0 : A => fst (fresp x0 y0))) q =
  idmap q) (class_of R a)) y intros; apply path_ishprop.
  Defined.

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

  Definition equiv_quotient_functor' (f : A <~> B)
    (fresp : forall 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. *)

  (** Because the statement uses nested Sigma types, we need several variables to serve as [max] and [u+1]. We write [ar] for [max(a,r)], [ar'] for [ar+1], etc. *)
  Universes a r ar ar' b ab abr.
  Constraint a <= ar, r <= ar, ar < ar', a <= ab, b <= ab, ab <= abr, ar <= abr.

  Context `{Funext}.

  (** A function we want to factor. *)
  Context {A : Type@{a}} {B : Type@{b}} `{IsHSet B} (f : A -> B).

  (** A mere Relation equivalent to its kernel. *)
  Context (R : Relation@{a r} A)
          (is_ker : forall x y, f x = f y <~> R x y).

  (** The factorization theorem.  An advantage of stating it as one bundled result is that it is easier to state variations as we do below.  Disadvantages are that it requires more universe variables and that each piece of the answer depends on [Funext] and all of the universe variables, even when these aren't needed for that piece.  Below we will clean up the universe variables slightly, so we make this version [Local]. *)
  Local Definition quotient_kernel_factor_internal
    : exists (C : Type@{ar}) (e : A -> C) (m : C -> B),
      IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e).
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
{C : Type &
{e : A -> C &
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = m o e)}}}
  Proof.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
{C : Type &
{e : A -> C &
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = m o e)}}}
    exists (Quotient R).
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
{e : A -> A / R &
{m : A / R -> B &
IsHSet (A / R) *
ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = (fun x : A => m (e x)))}}
    (* [exists (class_of R)] works, but the next line reduces the universe variables in a way that makes Coq 8.18 and 8.19 compatible. *)
    refine (exist@{ar abr} _ (class_of R) _).
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
{m : A / R -> B &
IsHSet (A / R) *
ReflectiveSubuniverse.IsConnMap (Tr (-1)) (class_of R) *
IsEmbedding m * (f = (fun x : A => m (class_of R x)))}
    srefine (_;_).
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
A / R -> B
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
(fun m : A / R -> B =>
 IsHSet (A / R) *
 ReflectiveSubuniverse.IsConnMap 
   (Tr (-1)) (class_of R) * 
 IsEmbedding m * (f = (fun x : A => m (class_of R x))))
  ?proj1
    {
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
A / R -> B refine (Quotient_ind R (fun _ => B) f _).
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
forall (x y : A) (H : R x y),
transport (fun _ : A / R => B) (qglue H) (f x) = f y
      intros x y p.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
x, y: A
p: R x y
transport (fun _ : A / R => B) (qglue p) (f x) = f y
      lhs nrapply transport_const.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
x, y: A
p: R x y
f x = f y
      exact ((is_ker x y)^-1 p). }
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
(fun m : A / R -> B =>
 IsHSet (A / R) *
 ReflectiveSubuniverse.IsConnMap (Tr (-1))
   (class_of R) * IsEmbedding m *
 (f = (fun x : A => m (class_of R x))))
  (Quotient_ind R (fun _ : A / R => B) f
     (fun (x y : A) (p : R x y) =>
      transport_const (qglue p) (f x) @
      (is_ker x y)^-1 p))
    repeat split; try exact _.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
IsEmbedding
  (Quotient_ind R (fun _ : A / R => B) f
     (fun (x y : A) (p : R x y) =>
      transport_const (qglue p) (f x) @
      (is_ker x y)^-1 p))
    intro u.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
IsHProp
  (hfiber
     (Quotient_ind R (fun _ : A / R => B) f
        (fun (x y : A) (p : R x y) =>
         transport_const (qglue p) (f x) @
         (is_ker x y)^-1 p)) u)
    apply hprop_allpath.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
forall
(x : hfiber
       (Quotient_ind R (fun _ : A / R => B) f
          (fun (x y : A) (p : R x y) =>
           transport_const (qglue p) (f x) @
           (is_ker x y)^-1 p)) u)
(y : hfiber
       (Quotient_ind R (fun _ : A / R => B) f
          (fun (x0 y : A) (p : R x0 y) =>
           transport_const (qglue p) (f x0) @
           (is_ker x0 y)^-1 p)) u), x = y
    intros [x q] [y p'].
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
x: A / R
q: Quotient_ind R (fun _ : A / R => B) f
  (fun (x y : A) (p : R x y) =>
   transport_const (qglue p) (f x) @
   (is_ker x y)^-1 p) x = u
y: A / R
p': Quotient_ind R (fun _ : A / R => B) f
  (fun (x y : A) (p : R x y) =>
   transport_const (qglue p) (f x) @
   (is_ker x y)^-1 p) y = u
(x; q) = (y; p')
    apply path_sigma_hprop; simpl.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
x: A / R
q: Quotient_ind R (fun _ : A / R => B) f
  (fun (x y : A) (p : R x y) =>
   transport_const (qglue p) (f x) @
   (is_ker x y)^-1 p) x = u
y: A / R
p': Quotient_ind R (fun _ : A / R => B) f
  (fun (x y : A) (p : R x y) =>
   transport_const (qglue p) (f x) @
   (is_ker x y)^-1 p) y = u
x = y
    revert x y q p'.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
forall x y : A / R,
Quotient_ind R (fun _ : A / R => B) f
  (fun (x0 y0 : A) (p : R x0 y0) =>
   transport_const (qglue p) (f x0) @
   (is_ker x0 y0)^-1 p) x = u ->
Quotient_ind R (fun _ : A / R => B) f
  (fun (x0 y0 : A) (p : R x0 y0) =>
   transport_const (qglue p) (f x0) @
   (is_ker x0 y0)^-1 p) y = u -> x = y
    srapply Quotient_ind.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
forall x : A,
(fun q : A / R =>
 forall y : A / R,
 Quotient_ind R (fun _ : A / R => B) f
   (fun (x0 y0 : A) (p : R x0 y0) =>
    transport_const (qglue p) (f x0) @
    (is_ker x0 y0)^-1 p) q = u ->
 Quotient_ind R (fun _ : A / R => B) f
   (fun (x0 y0 : A) (p : R x0 y0) =>
    transport_const (qglue p) (f x0) @
    (is_ker x0 y0)^-1 p) y = u -> q = y)
  (class_of R x)
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
forall (x y : A) (H0 : R x y),
transport
  (fun q : A / R =>
   forall y0 : A / R,
   Quotient_ind R (fun _ : A / R => B) f
     (fun (x0 y1 : A) (p : R x0 y1) =>
      transport_const (qglue p) (f x0) @
      (is_ker x0 y1)^-1 p) q = u ->
   Quotient_ind R (fun _ : A / R => B) f
     (fun (x0 y1 : A) (p : R x0 y1) =>
      transport_const (qglue p) (f x0) @
      (is_ker x0 y1)^-1 p) y0 = u -> 
   q = y0) (qglue H0) (?pclass x) = 
?pclass y
    2: intros; apply path_ishprop.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
forall x : A,
(fun q : A / R =>
 forall y : A / R,
 Quotient_ind R (fun _ : A / R => B) f
   (fun (x0 y0 : A) (p : R x0 y0) =>
    transport_const (qglue p) (f x0) @
    (is_ker x0 y0)^-1 p) q = u ->
 Quotient_ind R (fun _ : A / R => B) f
   (fun (x0 y0 : A) (p : R x0 y0) =>
    transport_const (qglue p) (f x0) @
    (is_ker x0 y0)^-1 p) y = u -> q = y)
  (class_of R x)
    intro a.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
a: A
(fun q : A / R =>
 forall y : A / R,
 Quotient_ind R (fun _ : A / R => B) f
   (fun (x y0 : A) (p : R x y0) =>
    transport_const (qglue p) (f x) @
    (is_ker x y0)^-1 p) q = u ->
 Quotient_ind R (fun _ : A / R => B) f
   (fun (x y0 : A) (p : R x y0) =>
    transport_const (qglue p) (f x) @
    (is_ker x y0)^-1 p) y = u -> q = y) (class_of R a)
    srapply Quotient_ind.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
a: A
forall x : A,
(fun q : A / R =>
 Quotient_ind R (fun _ : A / R => B) f
   (fun (x0 y : A) (p : R x0 y) =>
    transport_const (qglue p) (f x0) @
    (is_ker x0 y)^-1 p) (class_of R a) = u ->
 Quotient_ind R (fun _ : A / R => B) f
   (fun (x0 y : A) (p : R x0 y) =>
    transport_const (qglue p) (f x0) @
    (is_ker x0 y)^-1 p) q = u -> class_of R a = q)
  (class_of R x)
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
a: A
forall (x y : A) (H0 : R x y),
transport
  (fun q : A / R =>
   Quotient_ind R (fun _ : A / R => B) f
     (fun (x0 y0 : A) (p : R x0 y0) =>
      transport_const (qglue p) (f x0) @
      (is_ker x0 y0)^-1 p) 
     (class_of R a) = u ->
   Quotient_ind R (fun _ : A / R => B) f
     (fun (x0 y0 : A) (p : R x0 y0) =>
      transport_const (qglue p) (f x0) @
      (is_ker x0 y0)^-1 p) q = u -> 
   class_of R a = q) (qglue H0) 
  (?pclass x) = ?pclass y
    2: intros; apply path_ishprop.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
a: A
forall x : A,
(fun q : A / R =>
 Quotient_ind R (fun _ : A / R => B) f
   (fun (x0 y : A) (p : R x0 y) =>
    transport_const (qglue p) (f x0) @
    (is_ker x0 y)^-1 p) (class_of R a) = u ->
 Quotient_ind R (fun _ : A / R => B) f
   (fun (x0 y : A) (p : R x0 y) =>
    transport_const (qglue p) (f x0) @
    (is_ker x0 y)^-1 p) q = u -> class_of R a = q)
  (class_of R x)
    intros a' p p'.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
a, a': A
p: Quotient_ind R (fun _ : A / R => B) f
  (fun (x y : A) (p : R x y) =>
   transport_const (qglue p) (f x) @
   (is_ker x y)^-1 p) (class_of R a) = u
p': Quotient_ind R (fun _ : A / R => B) f
  (fun (x y : A) (p : R x y) =>
   transport_const (qglue p) (f x) @
   (is_ker x y)^-1 p) (class_of R a') = u
class_of R a = class_of R a'
    apply qglue, is_ker.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
is_ker: forall x y : A, f x = f y <~> R x y
u: B
a, a': A
p: Quotient_ind R (fun _ : A / R => B) f
  (fun (x y : A) (p : R x y) =>
   transport_const (qglue p) (f x) @
   (is_ker x y)^-1 p) (class_of R a) = u
p': Quotient_ind R (fun _ : A / R => B) f
  (fun (x y : A) (p : R x y) =>
   transport_const (qglue p) (f x) @
   (is_ker x y)^-1 p) (class_of R a') = u
f a = f a'
    exact (p @ p'^).
  Defined.

  (** We clean up the universe variables here, using only those declared in this Section. *)
  Definition quotient_kernel_factor_general@{|}
    := Eval unfold quotient_kernel_factor_internal in
      quotient_kernel_factor_internal@{ar' ar abr abr ab}.

End Kernel.

(** A common special case of [quotient_kernel_factor] is when we define [R] to be [f x = f y].  Then universes [r] and [b] are unified. *)
Definition quotient_kernel_factor@{a b ab ab' | a <= ab, b <= ab, ab < ab'}
  `{Funext} {A : Type@{a}} {B : Type@{b}} `{IsHSet B} (f : A -> B)
  : exists (C : Type@{ab}) (e : A -> C) (m : C -> B),
      IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e).
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
{C : Type &
{e : A -> C &
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = m o e)}}}
Proof.
H: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
{C : Type &
{e : A -> C &
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = m o e)}}}
  exact (quotient_kernel_factor_general@{a b ab ab' b ab ab}
           f (fun x y => f x = f y) (fun x y => equiv_idmap)).
Defined.

(** If we use propositional resizing, we can replace [f x = f y] with a proposition [R x y] in universe [a], so that the universe of [C] is the same as the universe of [A]. *)
Definition quotient_kernel_factor_small@{a a' b ab | a < a', a <= ab, b <= ab}
  `{Funext} `{PropResizing}
  {A : Type@{a}} {B : Type@{b}} `{IsHSet B} (f : A -> B)
  : exists (C : Type@{a}) (e : A -> C) (m : C -> B),
      IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e).
H: Funext
H0: PropResizing
A, B: Type
IsHSet0: IsHSet B
f: A -> B
{C : Type &
{e : A -> C &
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = m o e)}}}
Proof.
H: Funext
H0: PropResizing
A, B: Type
IsHSet0: IsHSet B
f: A -> B
{C : Type &
{e : A -> C &
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = m o e)}}}
  exact (quotient_kernel_factor_general@{a a a a' b ab ab}
           f (fun x y => resize_hprop@{b a} (f x = f y)) (fun x y => equiv_resize_hprop _)).
Defined.