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.

Set Universe Minimization ToSet.

Local Open Scope path_scope.

(** * The set-quotient of a type by a 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. 

Some results require additional assumptions, for example, that the relation be hprop-valued, or that the relation be reflexive, transitive or symmetric.

Throughout this file [a], [b] and [c] are elements of [A], [R] is a relation on [A], [x], [y] and [z] are elements of [Quotient R], [p] is a proof of [R a b].
*)

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} {a b : A}
  : R a b -> class_of@{i j k} R a = class_of R b
  := fun p => ap tr (gqglue p).

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 a, P (class_of R a))
  (peq : forall a b (H : R a b), qglue H # pclass a = pclass b)
  : forall x, P x.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
forall x : Quotient R, P x
Proof.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
forall x : Quotient R, P x
  rapply Trunc_ind; srapply GraphQuotient_ind.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
forall a : A,
(fun x : GraphQuotient R => P (tr x)) (gq a)
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
forall (a b : A) (s : R a b),
transport (fun x : GraphQuotient R => P (tr x))
  (gqglue s) (?gq' a) = 
?gq' b
  -
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
forall a : A,
(fun x : GraphQuotient R => P (tr x)) (gq a) exact pclass.
  -
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
forall (a b : A) (s : R a b),
transport (fun x : GraphQuotient R => P (tr x))
  (gqglue s) (pclass a) = pclass b intros a b p.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
a, b: A
p: R a b
transport (fun x : GraphQuotient R => P (tr x))
  (gqglue p) (pclass a) = pclass b
    lhs napply (transport_compose P).
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
a, b: A
p: R a b
transport P (ap tr (gqglue p)) (pclass a) = pclass b
    exact (peq a b p).
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 a, P (class_of R a))
  (peq : forall a b (H : R a b), qglue H # pclass a = pclass b)
  (a b : A) (p : R a b)
  : apD (Quotient_ind@{i j k l} R P pclass peq) (qglue p) = peq a b p.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
a, b: A
p: R a b
apD (Quotient_ind R P pclass peq) (qglue p) =
peq a b p
Proof.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
a, b: A
p: R a b
apD (Quotient_ind R P pclass peq) (qglue p) =
peq a b p
  lhs napply apD_compose'.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
a, b: A
p: R a b
(transport_compose P tr (gqglue p)
   (Quotient_ind R P pclass peq (tr (gq a))))^ @
apD
  (fun x : GraphQuotient R =>
   Quotient_ind R P pclass peq (tr x)) (gqglue p) =
peq a b p
  unfold Quotient_ind.
A: Type
R: Relation A
P: Quotient R -> Type
sP: forall x : Quotient R, IsHSet (P x)
pclass: forall a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
a, b: A
p: R a b
(transport_compose P tr (gqglue p)
   (Trunc_ind P
      (GraphQuotient_ind
         (fun x : GraphQuotient R => P (tr x)) pclass
         (fun (a b : A) (p : R a b) =>
          transport_compose P tr (gqglue p) (pclass a) @
          peq a b p)) (tr (gq a))))^ @
apD
  (fun x : GraphQuotient R =>
   Trunc_ind P
     (GraphQuotient_ind
        (fun x0 : GraphQuotient R => P (tr x0)) pclass
        (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 a b p
  nrefine (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 a : A, P (class_of R a)
peq: forall (a b : A) (H : R a b),
transport P (qglue H) (pclass a) = pclass b
a, b: A
p: R a b
(transport_compose P tr (gqglue p)
   (Trunc_ind P
      (GraphQuotient_ind
         (fun x : GraphQuotient R => P (tr x)) pclass
         (fun (a b : A) (p : R a b) =>
          transport_compose P tr (gqglue p) (pclass a) @
          peq a b p)) (tr (gq a))))^ @
(transport_compose P tr (gqglue p) (pclass a) @
 peq a b p) = peq a b 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 a b, R a b -> pclass a = pclass b)
  : Quotient@{i j k} R -> P.
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall a b : A, R a b -> pclass a = pclass b
Quotient R -> P
Proof.
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall a b : A, R a b -> pclass a = pclass b
Quotient R -> P
  srapply Trunc_rec; snapply GraphQuotient_rec.
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall a b : A, R a b -> pclass a = pclass b
A -> P
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall a b : A, R a b -> pclass a = pclass b
forall a b : A, R a b -> ?c a = ?c b
  -
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall a b : A, R a b -> pclass a = pclass b
A -> P exact pclass.
  -
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall a b : A, R a b -> pclass a = pclass b
forall a b : A, R a b -> pclass a = pclass b exact 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 a b, R a b -> pclass a = pclass b)
  (a b : A) (p : R a b)
  : ap (Quotient_rec@{i j k l} R P pclass peq) (qglue p) = peq a b p.
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall a b : A, R a b -> pclass a = pclass b
a, b: A
p: R a b
ap (Quotient_rec R P pclass peq) (qglue p) = peq a b p
Proof.
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall a b : A, R a b -> pclass a = pclass b
a, b: A
p: R a b
ap (Quotient_rec R P pclass peq) (qglue p) = peq a b p
  lhs_V napply (ap_compose tr).
A: Type
R: Relation A
P: Type
IsHSet0: IsHSet P
pclass: A -> P
peq: forall a b : A, R a b -> pclass a = pclass b
a, b: A
p: R a b
ap
  (fun x : GraphQuotient R =>
   Quotient_rec R P pclass peq (tr x)) (gqglue p) =
peq a b p
  snapply 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).

(** Quotient induction into an hprop. *)
Definition Quotient_ind_hprop {A : Type@{i}} (R : Relation@{i j} A)
  (P : A / R -> Type) `{forall x, IsHProp (P x)}
  (dclass : forall a, P (class_of R a))
  : forall x, P x.
A: Type
R: Relation A
P: A / R -> Type
H: forall x : A / R, IsHProp (P x)
dclass: forall a : A, P (class_of R a)
forall x : A / R, P x
Proof.
A: Type
R: Relation A
P: A / R -> Type
H: forall x : A / R, IsHProp (P x)
dclass: forall a : A, P (class_of R a)
forall x : A / R, P x
  srapply (Quotient_ind R P dclass).
A: Type
R: Relation A
P: A / R -> Type
H: forall x : A / R, IsHProp (P x)
dclass: forall a : A, P (class_of R a)
forall (a b : A) (H : R a b),
transport P (qglue H) (dclass a) = dclass b
  intros x y p; apply path_ishprop.
Defined.

Definition Quotient_ind2_hprop {A : Type@{i}} (R : Relation@{i j} A)
  (P : A / R -> A / R -> Type) `{forall x y, IsHProp (P x y)}
  (dclass : forall a b, P (class_of R a) (class_of R b))
  : forall x y, P x y.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: is_mere_relation (A / R) P
dclass: forall a b : A,
P (class_of R a) (class_of R b)
forall x y : A / R, P x y
Proof.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: is_mere_relation (A / R) P
dclass: forall a b : A,
P (class_of R a) (class_of R b)
forall x y : A / R, P x y
  intros x; srapply Quotient_ind_hprop; intros b.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: is_mere_relation (A / R) P
dclass: forall a b : A,
P (class_of R a) (class_of R b)
x: A / R
b: A
P x (class_of R b)
  revert x; srapply Quotient_ind_hprop; intros a.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: is_mere_relation (A / R) P
dclass: forall a b : A,
P (class_of R a) (class_of R b)
b, a: A
(fun x : A / R => P x (class_of R b)) (class_of R a)
  exact (dclass a b).
Defined.

Definition Quotient_ind3_hprop {A : Type@{i}} (R : Relation@{i j} A)
  (P : A / R -> A / R -> A / R -> Type) `{forall x y z, IsHProp (P x y z)}
  (dclass : forall a b c, P (class_of R a) (class_of R b) (class_of R c))
  : forall x y z, P x y z.
A: Type
R: Relation A
P: A / R -> A / R -> A / R -> Type
H: forall x y z : A / R, IsHProp (P x y z)
dclass: forall a b c : A,
P (class_of R a) (class_of R b)
  (class_of R c)
forall x y z : A / R, P x y z
Proof.
A: Type
R: Relation A
P: A / R -> A / R -> A / R -> Type
H: forall x y z : A / R, IsHProp (P x y z)
dclass: forall a b c : A,
P (class_of R a) (class_of R b)
  (class_of R c)
forall x y z : A / R, P x y z
  intros x; srapply Quotient_ind2_hprop; intros b c.
A: Type
R: Relation A
P: A / R -> A / R -> A / R -> Type
H: forall x y z : A / R, IsHProp (P x y z)
dclass: forall a b c : A,
P (class_of R a) (class_of R b)
  (class_of R c)
x: A / R
b, c: A
P x (class_of R b) (class_of R c)
  revert x; srapply Quotient_ind_hprop; intros a.
A: Type
R: Relation A
P: A / R -> A / R -> A / R -> Type
H: forall x y z : A / R, IsHProp (P x y z)
dclass: forall a b c : A,
P (class_of R a) (class_of R b)
  (class_of R c)
b, c, a: A
(fun x : A / R => P x (class_of R b) (class_of R c))
  (class_of R a)
  exact (dclass a b c).
Defined.

Definition Quotient_ind2 {A : Type} (R : Relation A)
  (P : A / R -> A / R -> Type) `{forall x y, IsHSet (P x y)}
  (dclass : forall a b, P (class_of R a) (class_of R b))
  (dequiv_l : forall a a' b (p : R a a'),
    transport (fun x => P x _) (qglue p) (dclass a b) = dclass a' b)
  (dequiv_r : forall a b b' (p : R b b'), qglue p # dclass a b = dclass a b')
  : forall x y, P x y.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
forall x y : A / R, P x y
Proof.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
forall x y : A / R, P x y
  intro x.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
x: A / R
forall y : A / R, P x y
  srapply Quotient_ind.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
x: A / R
forall a : A, P x (class_of R a)
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
x: A / R
forall (a b : A) (H0 : R a b),
transport (P x) (qglue H0) (?pclass a) = ?pclass b
  -
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
x: A / R
forall a : A, P x (class_of R a) intro b.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
x: A / R
b: A
P x (class_of R b)
    revert x.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
b: A
forall x : A / R, P x (class_of R b)
    srapply Quotient_ind.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
b: A
forall a : A,
(fun x : A / R => P x (class_of R b)) (class_of R a)
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
b: A
forall (a b0 : A) (H0 : R a b0),
transport (fun x : A / R => P x (class_of R b))
  (qglue H0) (?pclass a) = 
?pclass b0
    +
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
b: A
forall a : A,
(fun x : A / R => P x (class_of R b)) (class_of R a) intro a.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
b, a: A
(fun x : A / R => P x (class_of R b)) (class_of R a)
      exact (dclass a b).
    +
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
b: A
forall (a b0 : A) (H : R a b0),
transport (fun x : A / R => P x (class_of R b))
  (qglue H) ((fun a0 : A => dclass a0 b) a) =
(fun a0 : A => dclass a0 b) b0 cbn beta.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
b: A
forall (a b0 : A) (H : R a b0),
transport (fun x : A / R => P x (class_of R b))
  (qglue H) (dclass a b) = dclass b0 b
      intros a a' p.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
b, a, a': A
p: R a a'
transport (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = dclass a' b
      by apply dequiv_l.
  -
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
x: A / R
forall (a b : A) (H0 : R a b),
transport (P x) (qglue H0)
  ((fun b0 : A =>
    Quotient_ind R
      (fun x : A / R => P x (class_of R b0))
      (fun a0 : A => dclass a0 b0)
      ((fun (a0 a' : A) (p : R a0 a') =>
        dequiv_l a0 a' b0 p)
       :
       forall (a0 b1 : A) (H : R a0 b1),
       transport
         (fun x : A / R => P x (class_of R b0))
         (qglue H) ((fun a1 : A => dclass a1 b0) a0) =
       (fun a1 : A => dclass a1 b0) b1) x) a) =
(fun b0 : A =>
 Quotient_ind R (fun x : A / R => P x (class_of R b0))
   (fun a0 : A => dclass a0 b0)
   ((fun (a0 a' : A) (p : R a0 a') =>
     dequiv_l a0 a' b0 p)
    :
    forall (a0 b1 : A) (H : R a0 b1),
    transport (fun x : A / R => P x (class_of R b0))
      (qglue H) ((fun a1 : A => dclass a1 b0) a0) =
    (fun a1 : A => dclass a1 b0) b1) x) b cbn beta.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
x: A / R
forall (a b : A) (H0 : R a b),
transport (P x) (qglue H0)
  (Quotient_ind R
     (fun x : A / R => P x (class_of R a))
     (fun a0 : A => dclass a0 a)
     (fun (a0 a' : A) (p : R a0 a') =>
      dequiv_l a0 a' a p) x) =
Quotient_ind R (fun x : A / R => P x (class_of R b))
  (fun a0 : A => dclass a0 b)
  (fun (a0 a' : A) (p : R a0 a') => dequiv_l a0 a' b p)
  x
    intros b b' p.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
x: A / R
b, b': A
p: R b b'
transport (P x) (qglue p)
  (Quotient_ind R
     (fun x : A / R => P x (class_of R b))
     (fun a : A => dclass a b)
     (fun (a a' : A) (p : R a a') => dequiv_l a a' b p)
     x) =
Quotient_ind R (fun x : A / R => P x (class_of R b'))
  (fun a : A => dclass a b')
  (fun (a a' : A) (p : R a a') => dequiv_l a a' b' p)
  x
    revert x.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
b, b': A
p: R b b'
forall x : A / R,
transport (P x) (qglue p)
  (Quotient_ind R
     (fun x0 : A / R => P x0 (class_of R b))
     (fun a : A => dclass a b)
     (fun (a a' : A) (p : R a a') => dequiv_l a a' b p)
     x) =
Quotient_ind R
  (fun x0 : A / R => P x0 (class_of R b'))
  (fun a : A => dclass a b')
  (fun (a a' : A) (p : R a a') => dequiv_l a a' b' p)
  x
    srapply Quotient_ind_hprop; simpl.
A: Type
R: Relation A
P: A / R -> A / R -> Type
H: forall x y : A / R, IsHSet (P x y)
dclass: forall a b : A,
P (class_of R a) (class_of R b)
dequiv_l: forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R => P x (class_of R b))
  (qglue p) (dclass a b) = 
dclass a' b
dequiv_r: forall (a b b' : A) (p : R b b'),
transport (P (class_of R a)) 
  (qglue p) (dclass a b) = 
dclass a b'
b, b': A
p: R b b'
forall a : A,
transport (P (class_of R a)) (qglue p) (dclass a b) =
dclass a b'
    intro a; by apply dequiv_r.
Defined.

Definition Quotient_rec2 {A : Type} (R : Relation A) (B : Type) `{IsHSet B}
  (dclass : A -> A -> B)
  (dequiv_l : forall a a' b, R a a' -> dclass a b = dclass a' b)
  (dequiv_r : forall a b b', R b b' -> dclass a b = dclass a b')
  : A / R -> A / R -> B.
A: Type
R: Relation A
B: Type
IsHSet0: IsHSet B
dclass: A -> A -> B
dequiv_l: forall a a' b : A,
R a a' -> dclass a b = dclass a' b
dequiv_r: forall a b b' : A,
R b b' -> dclass a b = dclass a b'
A / R -> A / R -> B
Proof.
A: Type
R: Relation A
B: Type
IsHSet0: IsHSet B
dclass: A -> A -> B
dequiv_l: forall a a' b : A,
R a a' -> dclass a b = dclass a' b
dequiv_r: forall a b b' : A,
R b b' -> dclass a b = dclass a b'
A / R -> A / R -> B
  srapply Quotient_ind2.
A: Type
R: Relation A
B: Type
IsHSet0: IsHSet B
dclass: A -> A -> B
dequiv_l: forall a a' b : A,
R a a' -> dclass a b = dclass a' b
dequiv_r: forall a b b' : A,
R b b' -> dclass a b = dclass a b'
forall a b : A,
(fun _ _ : A / R => B) (class_of R a) (class_of R b)
A: Type
R: Relation A
B: Type
IsHSet0: IsHSet B
dclass: A -> A -> B
dequiv_l: forall a a' b : A,
R a a' -> dclass a b = dclass a' b
dequiv_r: forall a b b' : A,
R b b' -> dclass a b = dclass a b'
forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R =>
   (fun _ _ : A / R => B) x (class_of R b)) 
  (qglue p) (?dclass a b) = 
?dclass a' b
A: Type
R: Relation A
B: Type
IsHSet0: IsHSet B
dclass: A -> A -> B
dequiv_l: forall a a' b : A,
R a a' -> dclass a b = dclass a' b
dequiv_r: forall a b b' : A,
R b b' -> dclass a b = dclass a b'
forall (a b b' : A) (p : R b b'),
transport ((fun _ _ : A / R => B) (class_of R a))
  (qglue p) (?dclass a b) = 
?dclass a b'
  -
A: Type
R: Relation A
B: Type
IsHSet0: IsHSet B
dclass: A -> A -> B
dequiv_l: forall a a' b : A,
R a a' -> dclass a b = dclass a' b
dequiv_r: forall a b b' : A,
R b b' -> dclass a b = dclass a b'
forall a b : A,
(fun _ _ : A / R => B) (class_of R a) (class_of R b) exact dclass.
  -
A: Type
R: Relation A
B: Type
IsHSet0: IsHSet B
dclass: A -> A -> B
dequiv_l: forall a a' b : A,
R a a' -> dclass a b = dclass a' b
dequiv_r: forall a b b' : A,
R b b' -> dclass a b = dclass a b'
forall (a a' b : A) (p : R a a'),
transport
  (fun x : A / R =>
   (fun _ _ : A / R => B) x (class_of R b)) (qglue p)
  (dclass a b) = dclass a' b intros; lhs napply transport_const.
A: Type
R: Relation A
B: Type
IsHSet0: IsHSet B
dclass: A -> A -> B
dequiv_l: forall a a' b : A,
R a a' -> dclass a b = dclass a' b
dequiv_r: forall a b b' : A,
R b b' -> dclass a b = dclass a b'
a, a', b: A
p: R a a'
dclass a b = dclass a' b
    by apply dequiv_l.
  -
A: Type
R: Relation A
B: Type
IsHSet0: IsHSet B
dclass: A -> A -> B
dequiv_l: forall a a' b : A,
R a a' -> dclass a b = dclass a' b
dequiv_r: forall a b b' : A,
R b b' -> dclass a b = dclass a b'
forall (a b b' : A) (p : R b b'),
transport ((fun _ _ : A / R => B) (class_of R a))
  (qglue p) (dclass a b) = dclass a b' intros; lhs napply transport_const.
A: Type
R: Relation A
B: Type
IsHSet0: IsHSet B
dclass: A -> A -> B
dequiv_l: forall a a' b : A,
R a a' -> dclass a b = dclass a' b
dequiv_r: forall a b b' : A,
R b b' -> dclass a b = dclass a b'
a, b, b': A
p: R b b'
dclass a b = dclass a b'
    by apply dequiv_r.
Defined.

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. This requires [Univalence] so that we know that [HProp] is a set. *)
  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
    intros x b; revert 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
b: A
A / R -> HProp
    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
b: A
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
b: A
forall a b0 : A, R a b0 -> ?pclass a = ?pclass b0
    1: intro a; 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
b: A
forall a b0 : A,
R a b0 ->
(fun a0 : A => Build_HProp (R a0 b)) a =
(fun a0 : A => Build_HProp (R a0 b)) b0
    intros a c p; cbn beta.
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, a, c: A
p: R a c
Build_HProp (R a b) = Build_HProp (R c b)
    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
b, a, c: A
p: R a c
Build_HProp (R a b) <~> Build_HProp (R c b)
    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
b, a, c: A
p: R a c
R a b -> R c 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, a, c: A
p: R a c
R c b -> R a b
    1: exact (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
b, a, c: A
p: R a c
R c b -> R a b
    exact (transitivity p).
  Defined.

  (** Being in a class is decidable if the relation is decidable. *)
  #[export] Instance decidable_in_class `{forall a b, Decidable (R a b)}
  : 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 a b : A, Decidable (R a b)
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 a b : A, Decidable (R a b)
forall (x : A / R) (a : A), Decidable (in_class x a)
    by srapply Quotient_ind_hprop.
  Defined.

  (** If [a] is in a class [x], then the class of [a] is equal to [x]. *)
  Lemma path_in_class_of : forall x a, in_class x a -> x = class_of R 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
forall (x : A / R) (a : A),
in_class x a -> x = class_of R 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
forall (x : A / R) (a : A),
in_class x a -> x = class_of R a
    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 a : A,
(fun x : A / R =>
 forall a0 : A, in_class x a0 -> x = class_of R a0)
  (class_of R 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
forall (a b : A) (H3 : R a b),
transport
  (fun x : A / R =>
   forall a0 : A, in_class x a0 -> x = class_of R a0)
  (qglue H3) (?pclass a) = 
?pclass 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 a : A,
(fun x : A / R =>
 forall a0 : A, in_class x a0 -> x = class_of R a0)
  (class_of R a) intros a b 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
a, b: A
p: in_class (class_of R a) b
class_of R a = class_of R b
      exact (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 (a b : A) (H : R a b),
transport
  (fun x : A / R =>
   forall a0 : A, in_class x a0 -> x = class_of R a0)
  (qglue H)
  ((fun a0 : A =>
    (fun (b0 : A) (p : in_class (class_of R a0) b0) =>
     qglue p)
    :
    (fun x : A / R =>
     forall a1 : A, in_class x a1 -> x = class_of R a1)
      (class_of R a0)) a) =
(fun a0 : A =>
 (fun (b0 : A) (p : in_class (class_of R a0) b0) =>
  qglue p)
 :
 (fun x : A / R =>
  forall a1 : A, in_class x a1 -> x = class_of R a1)
   (class_of R a0)) b
    intros a b 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
a, b: A
p: R a b
transport
  (fun x : A / R =>
   forall a : A, in_class x a -> x = class_of R a)
  (qglue p)
  ((fun a : A =>
    (fun (b : A) (p : in_class (class_of R a) b) =>
     qglue p)
    :
    (fun x : A / R =>
     forall a0 : A, in_class x a0 -> x = class_of R a0)
      (class_of R a)) a) =
(fun a : A =>
 (fun (b : A) (p : in_class (class_of R a) b) =>
  qglue p)
 :
 (fun x : A / R =>
  forall a0 : A, in_class x a0 -> x = class_of R a0)
   (class_of R a)) b
    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
a, b: A
p: R a b
x: A
x0: in_class (class_of R b) x
transport
  (fun x : A / R =>
   forall a : A, in_class x a -> x = class_of R a)
  (qglue p)
  (fun (b : A) (p : in_class (class_of R a) b) =>
   qglue p) x x0 = qglue x0
    apply hset_path2.
  Defined.

  Lemma related_quotient_paths (a b : A)
    : class_of R a = class_of R b -> 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
a, b: A
class_of R a = class_of R b -> R a 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
a, b: A
class_of R a = class_of R b -> R a b
    intros 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
a, b: A
p: class_of R a = class_of R b
R a b
    change (in_class (class_of 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
a, b: A
p: class_of R a = class_of R b
in_class (class_of R a) b
    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
a, b: A
p: class_of R b = class_of R b
in_class (class_of R b) b
    cbv; reflexivity.
  Defined.

  (** Theorem 10.1.8. *)
  Theorem path_quotient (a b : A)
    : R a b <~> (class_of R a = class_of 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
a, b: A
R a b <~> class_of R a = class_of 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
a, b: A
R a b <~> class_of R a = class_of R b
    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
a, b: A
R a b -> class_of R a = class_of 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
a, b: A
class_of R a = class_of R b -> 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
a, b: A
R a b -> class_of R a = class_of R b exact 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
a, b: A
class_of R a = class_of R b -> R a b apply related_quotient_paths.
  Defined.

  (** The map [class_of : A -> A/R] is a surjection. *)
  #[export] 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 a : A,
(fun x : A / R =>
 trunctype_type (merely (hfiber (class_of R) x)))
  (class_of R a)
    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
a: A
(fun x : A / R =>
 trunctype_type (merely (hfiber (class_of R) x)))
  (class_of R a)
    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
a: A
hfiber (class_of R) (class_of R a)
    by exists a.
  Defined.

  (** The universal property of the quotient.  This is Lemma 6.10.3. *)
  Theorem equiv_quotient_ump (B : Type) `{IsHSet B}
    : (A / R -> B) <~> {f : A -> B & forall a b, R a b -> f a = f 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: Type
IsHSet0: IsHSet B
(A / R -> B) <~>
{f : A -> B & forall a b : A, R a b -> f a = f 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
B: Type
IsHSet0: IsHSet B
(A / R -> B) <~>
{f : A -> B & forall a b : A, R a b -> f a = f b}
    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: Type
IsHSet0: IsHSet B
(A / R -> B) ->
{f : A -> B & forall a b : A, R a b -> f a = f 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: Type
IsHSet0: IsHSet B
{f : A -> B & forall a b : A, R a b -> f a = f b} ->
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: Type
IsHSet0: IsHSet B
?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: Type
IsHSet0: IsHSet B
?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: Type
IsHSet0: IsHSet B
(A / R -> B) ->
{f : A -> B & forall a b : A, R a b -> f a = f b} 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: Type
IsHSet0: IsHSet B
f: A / R -> B
{f : A -> B & forall a b : A, R a b -> f a = f b}
      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: Type
IsHSet0: IsHSet B
f: A / R -> B
forall a b : A,
R a b -> f (class_of R a) = f (class_of R b)
      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: Type
IsHSet0: IsHSet B
f: A / R -> B
a, b: A
X: R a b
class_of R a = class_of R b
      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: Type
IsHSet0: IsHSet B
{f : A -> B & forall a b : A, R a b -> f a = f b} ->
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: Type
IsHSet0: IsHSet B
f: A -> B
H': forall a b : A, R a b -> f a = f b
A / R -> B
      exact (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: Type
IsHSet0: IsHSet B
(fun f : A / R -> B =>
 (fun x : A => f (class_of R x);
 fun (a b : A) (H : R a b) => ap11 1 (qglue H)))
o (fun
     X : {f : A -> B &
         forall a b : A, R a b -> f a = f b} =>
   (fun (f : A -> B)
      (H' : forall a b : A, R a b -> f a = f b) =>
    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: Type
IsHSet0: IsHSet B
f: A -> B
Hf: forall a b : A, R a b -> f a = f b
(fun x : A => Quotient_rec R B f Hf (class_of R x);
fun (a b : A) (H : R a b) => 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: Type
IsHSet0: IsHSet B
(fun
   X : {f : A -> B &
       forall a b : A, R a b -> f a = f b} =>
 (fun (f : A -> B)
    (H' : forall a b : A, R a b -> f a = f b) =>
  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 (a b : A) (H : R a b) => 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: Type
IsHSet0: IsHSet B
f: A / R -> B
Quotient_rec R B (fun x : A => f (class_of R x))
  (fun (a b : A) (H : R a b) => 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: Type
IsHSet0: IsHSet B
f: A / R -> B
Quotient_rec R B (fun x : A => f (class_of R x))
  (fun (a b : A) (H : R a b) => 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: Type
IsHSet0: IsHSet B
f: A / R -> B
forall a : A,
(fun x : A / R =>
 Quotient_rec R B (fun x0 : A => f (class_of R x0))
   (fun (a0 b : A) (H : R a0 b) => ap11 1 (qglue H)) x =
 f x) (class_of R a)
      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 a b, R a b -> S (f a) (f b))
    : Quotient R -> Quotient S.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b -> S (f a) (f b)
A / R -> B / S
  Proof.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b -> S (f a) (f b)
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 a b : A, R a b -> S (f a) (f b)
forall a b : A,
R a b -> class_of S (f a) = class_of S (f b)
    intros a b p.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b -> S (f a) (f b)
a, b: A
p: R a b
class_of S (f a) = class_of S (f b)
    apply qglue, fresp, p.
  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 a b, R a b -> S (f a) (f b))
    (g : B -> C) (gresp : forall a b, S a b -> T (g a) (g b))
    : Quotient_functor R T (g o f) (fun a b => (gresp _ _) o (fresp a b))
    == 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 a b : A, R a b -> S (f a) (f b)
g: B -> C
gresp: forall a b : B, S a b -> T (g a) (g b)
Quotient_functor R T (g o f)
  (fun a b : A => gresp (f a) (f b) o fresp a b) ==
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 a b : A, R a b -> S (f a) (f b)
g: B -> C
gresp: forall a b : B, S a b -> T (g a) (g b)
Quotient_functor R T (g o f)
  (fun a b : A => gresp (f a) (f b) o fresp a b) ==
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).

  #[export] Instance isequiv_quotient_functor (f : A -> B)
    (fresp : forall a b, R a b <-> S (f a) (f b)) `{IsEquiv _ _ f}
    : IsEquiv (Quotient_functor R S f (fun a b => fst (fresp a b))).
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
IsEquiv
  (Quotient_functor R S f
     (fun a b : A => fst (fresp a b)))
  Proof.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
IsEquiv
  (Quotient_functor R S f
     (fun a b : A => fst (fresp a b)))
    srapply (isequiv_adjointify _ (Quotient_functor S R f^-1 _)).
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
forall a b : B, S a b -> R (f^-1 a) (f^-1 b)
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
Quotient_functor R S f
  (fun a b : A => fst (fresp a b))
o Quotient_functor S R f^-1 ?fresp == idmap
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
Quotient_functor S R f^-1 ?fresp
o Quotient_functor R S f
    (fun a b : A => fst (fresp a b)) == idmap
    {
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
forall a b : B, S a b -> R (f^-1 a) (f^-1 b) intros a b s.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
a, b: B
s: S a b
R (f^-1 a) (f^-1 b)
      apply (snd (fresp _ _)).
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
a, b: B
s: S a b
S (f (f^-1 a)) (f (f^-1 b))
      abstract (do 2 rewrite eisretr; exact s). }
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
Quotient_functor R S f
  (fun a b : A => fst (fresp a b))
o Quotient_functor S R f^-1
    (fun (a b : B) (s : S a b) =>
     snd (fresp (f^-1 a) (f^-1 b))
       (isequiv_quotient_functor_subproof f H a b s)) ==
idmap
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
Quotient_functor S R f^-1
  (fun (a b : B) (s : S a b) =>
   snd (fresp (f^-1 a) (f^-1 b))
     (isequiv_quotient_functor_subproof f H a b s))
o Quotient_functor R S f
    (fun a b : A => fst (fresp a b)) == idmap
    all: srapply Quotient_ind.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
forall a : B,
(fun x : B / S =>
 (Quotient_functor R S f
    (fun a0 b : A => fst (fresp a0 b))
  o Quotient_functor S R f^-1
      (fun (a0 b : B) (s : S a0 b) =>
       snd (fresp (f^-1 a0) (f^-1 b))
         (isequiv_quotient_functor_subproof f H a0 b s)))
   x = idmap x) (class_of S a)
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
forall (a b : B) (H0 : S a b),
transport
  (fun x : B / S =>
   (Quotient_functor R S f
      (fun a0 b0 : A => fst (fresp a0 b0))
    o Quotient_functor S R f^-1
        (fun (a0 b0 : B) (s : S a0 b0) =>
         snd (fresp (f^-1 a0) (f^-1 b0))
           (isequiv_quotient_functor_subproof f H a0
              b0 s))) x = 
   idmap x) (qglue H0) (?pclass a) = 
?pclass b
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
forall a : A,
(fun x : A / R =>
 (Quotient_functor S R f^-1
    (fun (a0 b : B) (s : S a0 b) =>
     snd (fresp (f^-1 a0) (f^-1 b))
       (isequiv_quotient_functor_subproof f H a0 b s))
  o Quotient_functor R S f
      (fun a0 b : A => fst (fresp a0 b))) x = 
 idmap x) (class_of R a)
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
forall (a b : A) (H0 : R a b),
transport
  (fun x : A / R =>
   (Quotient_functor S R f^-1
      (fun (a0 b0 : B) (s : S a0 b0) =>
       snd (fresp (f^-1 a0) (f^-1 b0))
         (isequiv_quotient_functor_subproof f H a0 b0
            s))
    o Quotient_functor R S f
        (fun a0 b0 : A => fst (fresp a0 b0))) x =
   idmap x) (qglue H0) (?pclass0 a) = 
?pclass0 b
    +
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
forall a : B,
(fun x : B / S =>
 (Quotient_functor R S f
    (fun a0 b : A => fst (fresp a0 b))
  o Quotient_functor S R f^-1
      (fun (a0 b : B) (s : S a0 b) =>
       snd (fresp (f^-1 a0) (f^-1 b))
         (isequiv_quotient_functor_subproof f H a0 b s)))
   x = idmap x) (class_of S a) intros b; simpl.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
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 a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
forall (a b : B) (H0 : S a b),
transport
  (fun x : B / S =>
   (Quotient_functor R S f
      (fun a0 b0 : A => fst (fresp a0 b0))
    o Quotient_functor S R f^-1
        (fun (a0 b0 : B) (s : S a0 b0) =>
         snd (fresp (f^-1 a0) (f^-1 b0))
           (isequiv_quotient_functor_subproof f H a0
              b0 s))) x = idmap x) (qglue H0)
  ((fun b0 : B =>
    ap (class_of S) (eisretr f b0)
    :
    (fun x : B / S =>
     (Quotient_functor R S f
        (fun a0 b1 : A => fst (fresp a0 b1))
      o Quotient_functor S R f^-1
          (fun (a0 b1 : B) (s : S a0 b1) =>
           snd (fresp (f^-1 a0) (f^-1 b1))
             (isequiv_quotient_functor_subproof f H a0
                b1 s))) x = idmap x) (class_of S b0))
     a) =
(fun b0 : B =>
 ap (class_of S) (eisretr f b0)
 :
 (fun x : B / S =>
  (Quotient_functor R S f
     (fun a0 b1 : A => fst (fresp a0 b1))
   o Quotient_functor S R f^-1
       (fun (a0 b1 : B) (s : S a0 b1) =>
        snd (fresp (f^-1 a0) (f^-1 b1))
          (isequiv_quotient_functor_subproof f H a0 b1
             s))) x = idmap x) (class_of S b0)) b intros; apply path_ishprop.
    +
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
forall a : A,
(fun x : A / R =>
 (Quotient_functor S R f^-1
    (fun (a0 b : B) (s : S a0 b) =>
     snd (fresp (f^-1 a0) (f^-1 b))
       (isequiv_quotient_functor_subproof f H a0 b s))
  o Quotient_functor R S f
      (fun a0 b : A => fst (fresp a0 b))) x = idmap x)
  (class_of R a) intros a; simpl.
A: Type
R: Relation A
B: Type
S: Relation B
f: A -> B
fresp: forall a b : A, R a b <-> S (f a) (f b)
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 a b : A, R a b <-> S (f a) (f b)
H: IsEquiv f
forall (a b : A) (H0 : R a b),
transport
  (fun x : A / R =>
   (Quotient_functor S R f^-1
      (fun (a0 b0 : B) (s : S a0 b0) =>
       snd (fresp (f^-1 a0) (f^-1 b0))
         (isequiv_quotient_functor_subproof f H a0 b0
            s))
    o Quotient_functor R S f
        (fun a0 b0 : A => fst (fresp a0 b0))) x =
   idmap x) (qglue H0)
  ((fun a0 : A =>
    ap (class_of R) (eissect f a0)
    :
    (fun x : A / R =>
     (Quotient_functor S R f^-1
        (fun (a1 b0 : B) (s : S a1 b0) =>
         snd (fresp (f^-1 a1) (f^-1 b0))
           (isequiv_quotient_functor_subproof f H a1
              b0 s))
      o Quotient_functor R S f
          (fun a1 b0 : A => fst (fresp a1 b0))) x =
     idmap x) (class_of R a0)) a) =
(fun a0 : A =>
 ap (class_of R) (eissect f a0)
 :
 (fun x : A / R =>
  (Quotient_functor S R f^-1
     (fun (a1 b0 : B) (s : S a1 b0) =>
      snd (fresp (f^-1 a1) (f^-1 b0))
        (isequiv_quotient_functor_subproof f H a1 b0 s))
   o Quotient_functor R S f
       (fun a1 b0 : A => fst (fresp a1 b0))) x =
  idmap x) (class_of R a0)) b intros; apply path_ishprop.
  Defined.

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

  Definition equiv_quotient_functor' (f : A <~> B)
    (fresp : forall a b, R a b <-> S (f a) (f b))
    : 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).
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 (a b : A) (H : R a b),
transport (fun _ : A / R => B) (qglue H) (f a) = f b
      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 napply 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 a : A,
(fun x : 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) 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)
  (class_of R 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
forall (a b : A) (H0 : R a b),
transport
  (fun x : 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) 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) (qglue H0) (?pclass a) = 
?pclass b
    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 a : A,
(fun x : 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) 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)
  (class_of R a)
    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 x : 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) 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)
  (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 a0 : A,
(fun x : 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) x = u -> class_of R a = x)
  (class_of R a0)
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 (a0 b : A) (H0 : R a0 b),
transport
  (fun x : 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) x = u -> 
   class_of R a = x) (qglue H0) 
  (?pclass a0) = ?pclass b
    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 a0 : A,
(fun x : 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) x = u -> class_of R a = x)
  (class_of R a0)
    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 abr abr}.

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 a b => f a = f b) (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 a b => smalltype@{a b} (f a = f b))
           (fun x y => (equiv_smalltype _)^-1%equiv)).
Defined.