quotient.v

(* -*- mode: coq; mode: visual-line -*-  *)
Require Import HoTT.Basics HoTT.Types.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import HSet TruncType.
Require Import Truncations.Core.

Local Open Scope path_scope.

(** * The set-quotient of a type by an hprop-valued relation

We aim to model:
<<
Inductive quotient : Type :=
   | class_of : A -> quotient
   | related_classes_eq : forall x y, (R x y), class_of x = class_of y
   | quotient_set : IsHSet quotient
>>
*)

(** TODO:  This development should be further connected with the sections in the book; see below.  And it should be merged with Colimits.Quotient. Currently this file is only used in Classes/implementations/natpair_integers.v and Classes/implementations/field_of_fractions.v, so it shouldn't be too hard to switch to Colimits.Quotient. *)

Module Export Quotient.

  Section Domain.

    Universes i j u.
    Constraint i <= u, j <= u.

    Context {A : Type@{i}} (R : Relation@{i j} A) {sR: is_mere_relation _ R}.

    (** We choose to let the definition of quotient depend on the proof that [R] is a set-relations.  Alternatively, we could have defined it for all relations and only develop the theory for set-relations.  The former seems more natural.

We do not require [R] to be an equivalence relation, but implicitly consider its transitive-reflexive closure. *)

    (** This definition has a parameter [sR] that shadows the ambient one in the Context in order to ensure that it actually ends up depending on everything in the Context when the section is closed, since its definition doesn't actually refer to any of them.  *)
    Private Inductive quotient {sR: is_mere_relation _ R} : Type@{u} :=
    | class_of : A -> quotient.

    (** The path constructors. *)
    Axiom related_classes_eq
    : forall {x y : A}, R x y ->
                        class_of x = class_of y.

    Axiom quotient_set : IsHSet (@quotient sR).
    Global Existing Instance quotient_set.

    Definition quotient_ind (P : (@quotient sR) -> Type) {sP : forall x, IsHSet (P x)}
               (dclass : forall x, P (class_of x))
               (dequiv : (forall x y (H : R x y), (related_classes_eq H) # (dclass x) = dclass y))
    : forall q, P q
      := fun q => match q with class_of a => fun _ _ => dclass a end sP dequiv.

    Definition quotient_ind_compute {P sP} dclass dequiv x
    : @quotient_ind P sP dclass dequiv (class_of x) = dclass x.A: Type
R: Relation A
sR: is_mere_relation A R
P: quotient -> Type
sP: forall x : quotient, IsHSet (P x)
dclass: forall x : A, P (class_of x)
dequiv: forall (x y : A) (H : R x y),
transport P (related_classes_eq H) (dclass x) =
dclass y
x: A
quotient_ind P dclass dequiv (class_of x) = dclass x
    Proof.A: Type
R: Relation A
sR: is_mere_relation A R
P: quotient -> Type
sP: forall x : quotient, IsHSet (P x)
dclass: forall x : A, P (class_of x)
dequiv: forall (x y : A) (H : R x y),
transport P (related_classes_eq H) (dclass x) =
dclass y
x: A
quotient_ind P dclass dequiv (class_of x) = dclass x
      reflexivity.
    Defined.

    (** Again equality of paths needs to be postulated *)
    Axiom quotient_ind_compute_path
    : forall P sP dclass dequiv,
      forall x y (H : R x y),
        apD (@quotient_ind P sP dclass dequiv) (related_classes_eq H)
        = dequiv x y H.

  End Domain.

End Quotient.

Section Equiv.

  Context `{Univalence}.

  Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R}
          {Htrans : Transitive R} {Hsymm : Symmetric R}.

  Lemma quotient_path2 : forall {x y : quotient R} (p q : x=y), p=q.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
forall (x y : quotient R) (p q : x = y), p = q
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
forall (x y : quotient R) (p q : x = y), p = q
    apply @hset_path2.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
IsHSet (quotient R) apply _.
  Defined.

  Definition in_class : quotient R -> A -> HProp.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
quotient R -> A -> HProp
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
quotient R -> A -> HProp
    refine (quotient_ind R (fun _ => A -> HProp) (fun a b => Build_HProp (R a b)) _).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
forall (x y : A) (H : R x y),
transport (fun _ : quotient R => A -> HProp)
  (related_classes_eq R H)
  (fun b : A => Build_HProp (R x b)) =
(fun b : A => Build_HProp (R y b))
    intros.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
x, y: A
H0: R x y
transport (fun _ : quotient R => A -> HProp)
  (related_classes_eq R H0)
  (fun b : A => Build_HProp (R x b)) =
(fun b : A => Build_HProp (R y b)) eapply concat;[apply transport_const|].H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
x, y: A
H0: R x y
(fun b : A => Build_HProp (R x b)) =
(fun b : A => Build_HProp (R y b))
    apply path_forall.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
x, y: A
H0: R x y
(fun b : A => Build_HProp (R x b)) ==
(fun b : A => Build_HProp (R y b)) intro z.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
x, y: A
H0: R x y
z: A
Build_HProp (R x z) = Build_HProp (R y z) apply path_hprop; simpl.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
x, y: A
H0: R x y
z: A
R x z <~> R y z
    apply @equiv_iff_hprop; eauto.
  Defined.

  Context {Hrefl : Reflexive R}.

  Lemma in_class_pr : forall x y, (in_class (class_of R x) y : Type) = R x y.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall x y : A,
(in_class (class_of R x) y : Type) = R x y
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall x y : A,
(in_class (class_of R x) y : Type) = R x y
    reflexivity.
  Defined.

  Lemma quotient_ind_prop (P : quotient R -> Type)
        `{forall x, IsHProp (P x)} :
    forall dclass : forall x, P (class_of R x),
    forall q, P q.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
H0: forall x : quotient R, IsHProp (P x)
(forall x : A, P (class_of R x)) ->
forall q : quotient R, P q
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
H0: forall x : quotient R, IsHProp (P x)
(forall x : A, P (class_of R x)) ->
forall q : quotient R, P q
    intros.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
H0: forall x : quotient R, IsHProp (P x)
dclass: forall x : A, P (class_of R x)
q: quotient R
P q apply (quotient_ind R P dclass).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
H0: forall x : quotient R, IsHProp (P x)
dclass: forall x : A, P (class_of R x)
q: quotient R
forall (x y : A) (H : R x y),
transport P (related_classes_eq R H) (dclass x) =
dclass y
    intros.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
H0: forall x : quotient R, IsHProp (P x)
dclass: forall x : A, P (class_of R x)
q: quotient R
x, y: A
H1: R x y
transport P (related_classes_eq R H1) (dclass x) =
dclass y apply path_ishprop.
  Defined.

  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
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
H0: forall x y : A, Decidable (R x y)
forall (x : quotient R) (a : A),
Decidable (in_class x a)
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
H0: forall x y : A, Decidable (R x y)
forall (x : quotient R) (a : A),
Decidable (in_class x a)
    refine (quotient_ind_prop _ _).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
H0: forall x y : A, Decidable (R x y)
forall x a : A, Decidable (in_class (class_of R x) a)
    intros a b; exact (transport Decidable (in_class_pr a b) _).
  Defined.

  Lemma class_of_repr : forall q x, in_class q x -> q = class_of R x.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall (q : quotient R) (x : A),
in_class q x -> q = class_of R x
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall (q : quotient R) (x : A),
in_class q x -> q = class_of R x
    apply (quotient_ind R
                        (fun q : quotient R => forall x, in_class q x -> q = class_of _ x)
                        (fun x y H => related_classes_eq R H)).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall (x y : A) (H : R x y),
transport
  (fun q : quotient R =>
   forall x0 : A, in_class q x0 -> q = class_of R x0)
  (related_classes_eq R H)
  (fun (y0 : A) (H0 : in_class (class_of R x) y0) =>
   related_classes_eq R H0) =
(fun (y0 : A) (H0 : in_class (class_of R y) y0) =>
 related_classes_eq R H0)
    intros.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H0: R x y
transport
  (fun q : quotient R =>
   forall x : A, in_class q x -> q = class_of R x)
  (related_classes_eq R H0)
  (fun (y : A) (H : in_class (class_of R x) y) =>
   related_classes_eq R H) =
(fun (y0 : A) (H : in_class (class_of R y) y0) =>
 related_classes_eq R H)
    apply path_forall.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H0: R x y
transport
  (fun q : quotient R =>
   forall x : A, in_class q x -> q = class_of R x)
  (related_classes_eq R H0)
  (fun (y : A) (H : in_class (class_of R x) y) =>
   related_classes_eq R H) ==
(fun (y0 : A) (H : in_class (class_of R y) y0) =>
 related_classes_eq R H) intro z.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H0: R x y
z: A
transport
  (fun q : quotient R =>
   forall x : A, in_class q x -> q = class_of R x)
  (related_classes_eq R H0)
  (fun (y : A) (H : in_class (class_of R x) y) =>
   related_classes_eq R H) z =
(fun H : in_class (class_of R y) z =>
 related_classes_eq R H)
    apply path_forall;intro H'.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H0: R x y
z: A
H': in_class (class_of R y) z
transport
  (fun q : quotient R =>
   forall x : A, in_class q x -> q = class_of R x)
  (related_classes_eq R H0)
  (fun (y : A) (H : in_class (class_of R x) y) =>
   related_classes_eq R H) z H' =
related_classes_eq R H'
    apply quotient_path2.
  Defined.

  Lemma classes_eq_related : forall x y,
                               class_of R x = class_of R y -> R x y.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: 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
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall x y : A, class_of R x = class_of R y -> R x y
    intros x y H'.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H': class_of R x = class_of R y
R x y
    pattern (R x y).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H': class_of R x = class_of R y
idmap (R x y)
    eapply transport.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H': class_of R x = class_of R y
?T = R x y
H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H': class_of R x = class_of R y
?T
    -H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H': class_of R x = class_of R y
?T = R x y apply in_class_pr.
    -H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H': class_of R x = class_of R y
in_class (class_of R x) y pattern (class_of R x).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H': class_of R x = class_of R y
(fun q : quotient R => trunctype_type (in_class q y))
  (class_of R x) apply (transport _ (H'^)).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
H': class_of R x = class_of R y
in_class (class_of R y) y
      apply Hrefl.
  Defined.

  (** Thm 10.1.8 *)
  Theorem sets_exact : forall x y, (class_of R x = class_of R y) <~> R x y.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall x y : A, class_of R x = class_of R y <~> R x y
    intros ??.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
class_of R x = class_of R y <~> R x y apply equiv_iff_hprop.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
class_of R x = class_of R y -> R x y
H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
R x y -> class_of R x = class_of R y
    -H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
class_of R x = class_of R y -> R x y apply classes_eq_related.
    -H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x, y: A
R x y -> class_of R x = class_of R y apply related_classes_eq.
  Defined.

  Definition quotient_rec {B : Type} {sB : IsHSet B}
             (dclass : (forall x : A, B))
             (dequiv : (forall x y, R x y -> dclass x = dclass y))
  : quotient R -> B.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: Type
sB: IsHSet B
dclass: A -> B
dequiv: forall x y : A, R x y -> dclass x = dclass y
quotient R -> B
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: Type
sB: IsHSet B
dclass: A -> B
dequiv: forall x y : A, R x y -> dclass x = dclass y
quotient R -> B
    apply (quotient_ind R (fun _ : quotient _ => B)) with dclass.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: Type
sB: IsHSet B
dclass: A -> B
dequiv: forall x y : A, R x y -> dclass x = dclass y
forall (x y : A) (H : R x y),
transport (fun _ : quotient R => B)
  (related_classes_eq R H) (dclass x) = dclass y
    intros ?? H'.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: Type
sB: IsHSet B
dclass: A -> B
dequiv: forall x y : A, R x y -> dclass x = dclass y
x, y: A
H': R x y
transport (fun _ : quotient R => B)
  (related_classes_eq R H') (dclass x) = dclass y destruct (related_classes_eq R H').H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: Type
sB: IsHSet B
dclass: A -> B
dequiv: forall x y : A, R x y -> dclass x = dclass y
x, y: A
H': R x y
transport (fun _ : quotient R => B) 1 (dclass x) =
dclass y by apply dequiv.
  Defined.

  Definition quotient_rec2 {B : HSet} {dclass : (A -> A -> B)}:
    forall dequiv : (forall x x', R x x' -> forall y y',  R y y' ->
                                                          dclass x y = dclass x' y'),
      quotient R -> quotient R -> B.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
dclass: A -> A -> B
(forall x x' : A,
 R x x' ->
 forall y y' : A, R y y' -> dclass x y = dclass x' y') ->
quotient R -> quotient R -> B
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
dclass: A -> A -> B
(forall x x' : A,
 R x x' ->
 forall y y' : A, R y y' -> dclass x y = dclass x' y') ->
quotient R -> quotient R -> B
    intro.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
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'
quotient R -> quotient R -> B
    assert (dequiv0 : forall x x0 y : A, R x0 y -> dclass x x0 = dclass x y)
      by (intros ? ? ? Hx; apply dequiv;[apply Hrefl|done]).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
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'
dequiv0: forall x x0 y : A,
R x0 y -> dclass x x0 = dclass x y
quotient R -> quotient R -> B
    refine (quotient_rec
              (fun x => quotient_rec (dclass x) (dequiv0 x)) _).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
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'
dequiv0: forall x x0 y : A,
R x0 y -> dclass x x0 = dclass x y
forall x y : A,
R x y ->
quotient_rec (dclass x) (dequiv0 x) =
quotient_rec (dclass y) (dequiv0 y)
    intros x x' Hx.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
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'
dequiv0: forall x x0 y : A,
R x0 y -> dclass x x0 = dclass x y
x, x': A
Hx: R x x'
quotient_rec (dclass x) (dequiv0 x) =
quotient_rec (dclass x') (dequiv0 x')
    apply path_forall.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
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'
dequiv0: forall x x0 y : A,
R x0 y -> dclass x x0 = dclass x y
x, x': A
Hx: R x x'
quotient_rec (dclass x) (dequiv0 x) ==
quotient_rec (dclass x') (dequiv0 x') red.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
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'
dequiv0: forall x x0 y : A,
R x0 y -> dclass x x0 = dclass x y
x, x': A
Hx: R x x'
forall x0 : quotient R,
quotient_rec (dclass x) (dequiv0 x) x0 =
quotient_rec (dclass x') (dequiv0 x') x0
    assert (dequiv1 : forall y : A,
                        quotient_rec (dclass x) (dequiv0 x) (class_of _ y) =
                        quotient_rec (dclass x') (dequiv0 x') (class_of _ y))
      by (intros; by apply dequiv).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
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'
dequiv0: forall x x0 y : A,
R x0 y -> dclass x x0 = dclass x y
x, x': A
Hx: R x x'
dequiv1: forall y : A,
quotient_rec (dclass x) 
  (dequiv0 x) (class_of R y) =
quotient_rec (dclass x') 
  (dequiv0 x') (class_of R y)
forall x0 : quotient R,
quotient_rec (dclass x) (dequiv0 x) x0 =
quotient_rec (dclass x') (dequiv0 x') x0
    refine (quotient_ind R (fun q =>
                              quotient_rec (dclass x) (dequiv0 x) q =
                              quotient_rec (dclass x') (dequiv0 x') q) dequiv1 _).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
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'
dequiv0: forall x x0 y : A,
R x0 y -> dclass x x0 = dclass x y
x, x': A
Hx: R x x'
dequiv1: forall y : A,
quotient_rec (dclass x) 
  (dequiv0 x) (class_of R y) =
quotient_rec (dclass x') 
  (dequiv0 x') (class_of R y)
forall (x0 y : A) (H : R x0 y),
transport
  (fun q : quotient R =>
   quotient_rec (dclass x) (dequiv0 x) q =
   quotient_rec (dclass x') (dequiv0 x') q)
  (related_classes_eq R H) (dequiv1 x0) = dequiv1 y
    intros.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
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'
dequiv0: forall x x0 y : A,
R x0 y -> dclass x x0 = dclass x y
x, x': A
Hx: R x x'
dequiv1: forall y : A,
quotient_rec (dclass x) 
  (dequiv0 x) (class_of R y) =
quotient_rec (dclass x') 
  (dequiv0 x') (class_of R y)
x0, y: A
H0: R x0 y
transport
  (fun q : quotient R =>
   quotient_rec (dclass x) (dequiv0 x) q =
   quotient_rec (dclass x') (dequiv0 x') q)
  (related_classes_eq R H0) (dequiv1 x0) = dequiv1 y apply path_ishprop.
  Defined.

  Definition quotient_ind_prop' : forall P : quotient R -> Type,
                                  forall (Hprop' : forall x, IsHProp (P (class_of _ x))),
                                    (forall x, P (class_of _ x)) -> forall y, P y.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall P : quotient R -> Type,
(forall x : A, IsHProp (P (class_of R x))) ->
(forall x : A, P (class_of R x)) ->
forall y : quotient R, P y
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall P : quotient R -> Type,
(forall x : A, IsHProp (P (class_of R x))) ->
(forall x : A, P (class_of R x)) ->
forall y : quotient R, P y
    intros ? ? dclass.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
Hprop': forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall y : quotient R, P y apply quotient_ind with dclass.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
Hprop': forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall x : quotient R, IsHSet (P x)
H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
Hprop': 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 (related_classes_eq R H) (dclass x) =
dclass y
    -H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
Hprop': forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
forall x : quotient R, IsHSet (P x) simple refine (quotient_ind R (fun x => IsHSet (P x)) _ _); cbn beta; try exact _.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
Hprop': 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 x0 : quotient R => IsHSet (P x0))
  (related_classes_eq R H)
  ((fun x0 : A => istrunc_hprop) x) =
(fun x0 : A => istrunc_hprop) y
      intros; apply path_ishprop.
    -H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
Hprop': 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 (related_classes_eq R H) (dclass x) =
dclass y intros.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
P: quotient R -> Type
Hprop': forall x : A, IsHProp (P (class_of R x))
dclass: forall x : A, P (class_of R x)
x, y: A
H0: R x y
transport P (related_classes_eq R H0) (dclass x) =
dclass y apply path_ishprop.
  Defined.

  (** From Ch6 *)
  Theorem quotient_surjective: IsSurjection (class_of R).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
ReflectiveSubuniverse.IsConnMap (Tr (-1)) (class_of R)
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
ReflectiveSubuniverse.IsConnMap (Tr (-1)) (class_of R)
    apply BuildIsSurjection.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall b : quotient R, merely (hfiber (class_of R) b)
    apply (quotient_ind_prop (fun y => merely (hfiber (class_of R) y))); try exact _.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
forall x : A,
merely (hfiber (class_of R) (class_of R x))
    intro x.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x: A
merely (hfiber (class_of R) (class_of R x)) apply tr.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
x: A
hfiber (class_of R) (class_of R x) by exists x.
  Defined.

  (** From Ch10 *)
  Definition quotient_ump' (B:HSet): (quotient R -> B) ->
                                     (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
(quotient R -> B) ->
{f : A -> B & forall a a0 : A, R a a0 -> f a = f a0}
    intro f.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
f: quotient R -> B
{f : A -> B & forall a a0 : A, R a a0 -> f a = f a0} exists (compose f (class_of R) ).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
f: quotient R -> B
forall a a0 : A,
R a a0 -> f (class_of R a) = f (class_of R a0)
    intros.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
f: quotient R -> B
a, a0: A
X: R a a0
f (class_of R a) = f (class_of R a0) f_ap.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
f: quotient R -> B
a, a0: A
X: R a a0
class_of R a = class_of R a0 by apply related_classes_eq.
  Defined.

  Definition quotient_ump'' (B:HSet): (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0)))
                                      -> quotient R -> B.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
{f : A -> B & forall a a0 : A, R a a0 -> f a = f a0} ->
quotient R -> B
    intros [f H'].H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
f: A -> B
H': forall a a0 : A, R a a0 -> f a = f a0
quotient R -> B
    apply (quotient_rec _ H').
  Defined.

  Theorem quotient_ump (B:HSet): (quotient R -> B) <~>
                                                   (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
(quotient R -> B) <~>
{f : A -> B & forall a a0 : A, R a a0 -> f a = f a0}
  Proof.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
(quotient R -> B) <~>
{f : A -> B & forall a a0 : A, R a a0 -> f a = f a0}
    refine (equiv_adjointify (quotient_ump' B) (quotient_ump'' B) _ _).H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
(fun
   x : {f : A -> B &
       forall a a0 : A, R a a0 -> f a = f a0} =>
 quotient_ump' B (quotient_ump'' B x)) == idmap
H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
(fun x : quotient R -> B =>
 quotient_ump'' B (quotient_ump' B x)) == idmap
    -H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
(fun
   x : {f : A -> B &
       forall a a0 : A, R a a0 -> f a = f a0} =>
 quotient_ump' B (quotient_ump'' B x)) == idmap intros [f Hf].H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
f: A -> B
Hf: forall a a0 : A, R a a0 -> f a = f a0
quotient_ump' B (quotient_ump'' B (f; Hf)) = (f; Hf)
      by apply equiv_path_sigma_hprop.
    -H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
(fun x : quotient R -> B =>
 quotient_ump'' B (quotient_ump' B x)) == idmap intros f.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
f: quotient R -> B
quotient_ump'' B (quotient_ump' B f) = f
      apply path_forall.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
f: quotient R -> B
quotient_ump'' B (quotient_ump' B f) == f
      red.H: Univalence
A: Type
R: Relation A
sR: is_mere_relation A R
Htrans: Transitive R
Hsymm: Symmetric R
Hrefl: Reflexive R
B: HSet
f: quotient R -> B
forall x : quotient R,
quotient_ump'' B (quotient_ump' B f) x = f x apply quotient_ind_prop';[apply _|reflexivity].
  Defined.

  (** Missing

  The equivalence with VVquotient [A//R].

  This should lead to the unnamed theorem:

  10.1.10. Equivalence relations are effective and there is an equivalence [A/R<~>A//R]. *)

  (**
  The theory of canonical quotients is developed by C.Cohen:
  http://perso.crans.org/cohen/work/quotients/
 *)

End Equiv.

Section Functoriality.

  Definition quotient_functor
             {A : Type} (R : Relation A) {sR: is_mere_relation _ R}
             {B : Type} (S : Relation B) {sS: is_mere_relation _ S}
             (f : A -> B) (fresp : forall x y, R x y -> S (f x) (f y))
  : quotient R -> quotient S.A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
f: A -> B
fresp: forall x y : A, R x y -> S (f x) (f y)
quotient R -> quotient S
  Proof.A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
f: A -> B
fresp: forall x y : A, R x y -> S (f x) (f y)
quotient R -> quotient S
    refine (quotient_rec R (class_of S o f) _).A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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 related_classes_eq, fresp, r.
  Defined.

  Context {A : Type} (R : Relation A) {sR: is_mere_relation _ R}
          {B : Type} (S : Relation B) {sS: is_mere_relation _ S}.

  Global Instance quotient_functor_isequiv
             (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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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)))
    simple refine (isequiv_adjointify _ (quotient_functor S R f^-1 _)
                               _ _).A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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))
       (quotient_functor_isequiv_subproof f H u v s)) ==
idmap intros x; revert x; simple refine (quotient_ind S _ _ _).A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall x : B,
(fun q : quotient S =>
 quotient_functor R S f
   (fun x0 y : A => fst (fresp x0 y))
   (quotient_functor S R f^-1
      (fun (u v : B) (s : S u v) =>
       snd (fresp (f^-1 u) (f^-1 v))
         (quotient_functor_isequiv_subproof f H u v s))
      q) = q) (class_of S x)
A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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 : quotient S =>
   quotient_functor R S f
     (fun x0 y0 : A => fst (fresp x0 y0))
     (quotient_functor S R f^-1
        (fun (u v : B) (s : S u v) =>
         snd (fresp (f^-1 u) (f^-1 v))
           (quotient_functor_isequiv_subproof f H u v
              s)) q) = q) 
  (related_classes_eq S H0) 
  (?dclass x) = ?dclass y
      +A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall x : B,
(fun q : quotient S =>
 quotient_functor R S f
   (fun x0 y : A => fst (fresp x0 y))
   (quotient_functor S R f^-1
      (fun (u v : B) (s : S u v) =>
       snd (fresp (f^-1 u) (f^-1 v))
         (quotient_functor_isequiv_subproof f H u v s))
      q) = q) (class_of S x) intros b; simpl.A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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 : quotient S =>
   quotient_functor R S f
     (fun x0 y0 : A => fst (fresp x0 y0))
     (quotient_functor S R f^-1
        (fun (u v : B) (s : S u v) =>
         snd (fresp (f^-1 u) (f^-1 v))
           (quotient_functor_isequiv_subproof f H u v
              s)) q) = q) (related_classes_eq S H0)
  ((fun b : B =>
    ap (class_of S) (eisretr f b)
    :
    (fun q : quotient S =>
     quotient_functor R S f
       (fun x0 y0 : A => fst (fresp x0 y0))
       (quotient_functor S R f^-1
          (fun (u v : B) (s : S u v) =>
           snd (fresp (f^-1 u) (f^-1 v))
             (quotient_functor_isequiv_subproof f H u
                v s)) q) = q) (class_of S b)) x) =
(fun b : B =>
 ap (class_of S) (eisretr f b)
 :
 (fun q : quotient S =>
  quotient_functor R S f
    (fun x0 y0 : A => fst (fresp x0 y0))
    (quotient_functor S R f^-1
       (fun (u v : B) (s : S u v) =>
        snd (fresp (f^-1 u) (f^-1 v))
          (quotient_functor_isequiv_subproof f H u v s))
       q) = q) (class_of S b)) y intros; apply path_ishprop.
    -A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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))
     (quotient_functor_isequiv_subproof f H u v s))
o quotient_functor R S f
    (fun x y : A => fst (fresp x y)) == idmap intros x; revert x; simple refine (quotient_ind R _ _ _).A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall x : A,
(fun q : quotient R =>
 quotient_functor S R f^-1
   (fun (u v : B) (s : S u v) =>
    snd (fresp (f^-1 u) (f^-1 v))
      (quotient_functor_isequiv_subproof f H u v s))
   (quotient_functor R S f
      (fun x0 y : A => fst (fresp x0 y)) q) = q)
  (class_of R x)
A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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 : quotient R =>
   quotient_functor S R f^-1
     (fun (u v : B) (s : S u v) =>
      snd (fresp (f^-1 u) (f^-1 v))
        (quotient_functor_isequiv_subproof f H u v s))
     (quotient_functor R S f
        (fun x0 y0 : A => fst (fresp x0 y0)) q) = q)
  (related_classes_eq R H0) 
  (?dclass x) = ?dclass y
      +A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
f: A -> B
fresp: forall x y : A, R x y <-> S (f x) (f y)
H: IsEquiv f
forall x : A,
(fun q : quotient R =>
 quotient_functor S R f^-1
   (fun (u v : B) (s : S u v) =>
    snd (fresp (f^-1 u) (f^-1 v))
      (quotient_functor_isequiv_subproof f H u v s))
   (quotient_functor R S f
      (fun x0 y : A => fst (fresp x0 y)) q) = q)
  (class_of R x) intros a; simpl.A: Type
R: Relation A
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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
sR: is_mere_relation A R
B: Type
S: Relation B
sS: is_mere_relation B S
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 : quotient R =>
   quotient_functor S R f^-1
     (fun (u v : B) (s : S u v) =>
      snd (fresp (f^-1 u) (f^-1 v))
        (quotient_functor_isequiv_subproof f H u v s))
     (quotient_functor R S f
        (fun x0 y0 : A => fst (fresp x0 y0)) q) = q)
  (related_classes_eq R H0)
  ((fun a : A =>
    ap (class_of R) (eissect f a)
    :
    (fun q : quotient R =>
     quotient_functor S R f^-1
       (fun (u v : B) (s : S u v) =>
        snd (fresp (f^-1 u) (f^-1 v))
          (quotient_functor_isequiv_subproof f H u v s))
       (quotient_functor R S f
          (fun x0 y0 : A => fst (fresp x0 y0)) q) = q)
      (class_of R a)) x) =
(fun a : A =>
 ap (class_of R) (eissect f a)
 :
 (fun q : quotient R =>
  quotient_functor S R f^-1
    (fun (u v : B) (s : S u v) =>
     snd (fresp (f^-1 u) (f^-1 v))
       (quotient_functor_isequiv_subproof f H u v s))
    (quotient_functor R S f
       (fun x0 y0 : A => fst (fresp x0 y0)) q) = q)
   (class_of R a)) y intros; apply path_ishprop.
  Defined.

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

  Definition quotient_functor_equiv'
             (f : A <~> B) (fresp : forall x y, R x y <-> S (f x) (f y))
  : quotient R <~> quotient S
    := quotient_functor_equiv f fresp.

End Functoriality.

Section Kernel.

  (** ** Quotients of kernels of maps to sets give a surjection/mono factorization. *)

  Context {fs : Funext}.

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

  (** A mere relation equivalent to its kernel. *)
  Context (R : Relation A) {sR : is_mere_relation _ R}.
  Context (is_ker : forall x y, f x = f y <~> R x y).

  Theorem quotient_kernel_factor
  : exists (C : Type) (e : A -> C) (m : C -> B),
      IsHSet C * IsSurjection e * IsEmbedding m * (f = m o e).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
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.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
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)}}}
    pose (C := quotient R).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
{C : Type &
{e : A -> C &
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = m o e)}}}
    (* We put this explicitly in the context so that typeclass resolution will pick it up. *)
    assert (IsHSet C) by (unfold C; apply _).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
{C : Type &
{e : A -> C &
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = m o e)}}}
    exists C.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
{e : A -> C &
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = (fun x : A => m (e x)))}}
    pose (e := class_of R).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
{e : A -> C &
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = (fun x : A => m (e x)))}}
    exists e.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = (fun x : A => m (e x)))}
    transparent assert (m : (C -> B)).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
C -> B
fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= ?Goal: C -> B
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = (fun x : A => m (e x)))}
    {fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
C -> B apply quotient_ind with f; try exact _.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
forall (x y : A) (H : R x y),
transport (fun _ : quotient R => B)
  (related_classes_eq R H) (f x) = f y
      intros x y H.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
x, y: A
H: R x y
transport (fun _ : quotient R => B)
  (related_classes_eq R H) (f x) = f y transitivity (f x).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
x, y: A
H: R x y
transport (fun _ : quotient R => B)
  (related_classes_eq R H) (f x) = f x
fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
x, y: A
H: R x y
f x = f y
      -fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
x, y: A
H: R x y
transport (fun _ : quotient R => B)
  (related_classes_eq R H) (f x) = f x apply transport_const.
      -fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
x, y: A
H: R x y
f x = f y exact ((is_ker x y) ^-1 H). }fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
{m : C -> B &
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = (fun x : A => m (e x)))}
    exists m.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
IsHSet C * ReflectiveSubuniverse.IsConnMap (Tr (-1)) e *
IsEmbedding m * (f = (fun x : A => m (e x)))
    split;[split;[split|]|].fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
IsHSet C
fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
ReflectiveSubuniverse.IsConnMap (Tr (-1)) e
fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
IsEmbedding m
fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
f = (fun x : A => m (e x))
    -fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
IsHSet C assumption.
    -fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
ReflectiveSubuniverse.IsConnMap (Tr (-1)) e apply quotient_surjective.
    -fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
IsEmbedding m intro u.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
IsHProp (hfiber m u)
      apply hprop_allpath.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
forall x y : hfiber m u, x = y
      assert (H : forall (x y : C) (p : m x = u) (p' : m y = u), x = y).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
forall x y : C, m x = u -> m y = u -> x = y
fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
H: forall x y : C, m x = u -> m y = u -> x = y
forall x y : hfiber m u, x = y
      {fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
forall x y : C, m x = u -> m y = u -> x = y simple refine (quotient_ind R _ _ _).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
forall x : A,
(fun q : quotient R =>
 forall y : C, m q = u -> m y = u -> q = y)
  (class_of R x)
fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
forall (x y : A) (H : R x y),
transport
  (fun q : quotient R =>
   forall y0 : C, m q = u -> m y0 = u -> q = y0)
  (related_classes_eq R H) 
  (?dclass x) = ?dclass y
        -fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
forall x : A,
(fun q : quotient R =>
 forall y : C, m q = u -> m y = u -> q = y)
  (class_of R x) intro a.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
a: A
(fun q : quotient R =>
 forall y : C, m q = u -> m y = u -> q = y)
  (class_of R a)
          simple refine (quotient_ind R _ _ _).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
a: A
forall x : A,
(fun q : quotient R =>
 m (class_of R a) = u -> m q = u -> class_of R a = q)
  (class_of R x)
fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
a: A
forall (x y : A) (H : R x y),
transport
  (fun q : quotient R =>
   m (class_of R a) = u -> m q = u -> class_of R a = q)
  (related_classes_eq R H) 
  (?dclass x) = ?dclass y
          +fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
a: A
forall x : A,
(fun q : quotient R =>
 m (class_of R a) = u -> m q = u -> class_of R a = q)
  (class_of R x) intros a' p p'; fold e in p, p'.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
a, a': A
p: m (e a) = u
p': m (e a') = u
class_of R a = class_of R a'
            *fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
a, a': A
p: m (e a) = u
p': m (e a') = u
class_of R a = class_of R a' apply related_classes_eq.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
a, a': A
p: m (e a) = u
p': m (e a') = u
R a a'
              refine (is_ker a a' _).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
a, a': A
p: m (e a) = u
p': m (e a') = u
f a = f a'
              change (m (e a) = m (e a')).fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
a, a': A
p: m (e a) = u
p': m (e a') = u
m (e a) = m (e a')
              exact (p @ p'^).
          +fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
a: A
forall (x y : A) (H : R x y),
transport
  (fun q : quotient R =>
   m (class_of R a) = u -> m q = u -> class_of R a = q)
  (related_classes_eq R H)
  ((fun a' : A =>
    (fun (p : m (class_of R a) = u)
       (p' : m (class_of R a') = u) =>
     related_classes_eq R (is_ker a a' (p @ p'^)))
    :
    (fun q : quotient R =>
     m (class_of R a) = u ->
     m q = u -> class_of R a = q) (class_of R a')) x) =
(fun a' : A =>
 (fun (p : m (class_of R a) = u)
    (p' : m (class_of R a') = u) =>
  related_classes_eq R (is_ker a a' (p @ p'^)))
 :
 (fun q : quotient R =>
  m (class_of R a) = u -> m q = u -> class_of R a = q)
   (class_of R a')) y intros; apply path_ishprop.
        -fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
forall (x y : A) (H : R x y),
transport
  (fun q : quotient R =>
   forall y0 : C, m q = u -> m y0 = u -> q = y0)
  (related_classes_eq R H)
  ((fun a : A =>
    quotient_ind R
      (fun q : quotient R =>
       m (class_of R a) = u ->
       m q = u -> class_of R a = q)
      (fun a' : A =>
       (fun (p : m (class_of R a) = u)
          (p' : m (class_of R a') = u) =>
        related_classes_eq R (is_ker a a' (p @ p'^)))
       :
       (fun q : quotient R =>
        m (class_of R a) = u ->
        m q = u -> class_of R a = q) (class_of R a'))
      (fun (x0 y0 : A) (H0 : R x0 y0) =>
       path_ishprop
         (transport
            (fun q : quotient R =>
             m (class_of R a) = u ->
             m q = u -> class_of R a = q)
            (related_classes_eq R H0)
            (fun (p : m (class_of R a) = u)
               (p' : m (class_of R x0) = u) =>
             related_classes_eq R
               (is_ker a x0 (p @ p'^))))
         (fun (p : m (class_of R a) = u)
            (p' : m (class_of R y0) = u) =>
          related_classes_eq R (is_ker a y0 (p @ p'^)))))
     x) =
(fun a : A =>
 quotient_ind R
   (fun q : quotient R =>
    m (class_of R a) = u ->
    m q = u -> class_of R a = q)
   (fun a' : A =>
    (fun (p : m (class_of R a) = u)
       (p' : m (class_of R a') = u) =>
     related_classes_eq R (is_ker a a' (p @ p'^)))
    :
    (fun q : quotient R =>
     m (class_of R a) = u ->
     m q = u -> class_of R a = q) (class_of R a'))
   (fun (x0 y0 : A) (H0 : R x0 y0) =>
    path_ishprop
      (transport
         (fun q : quotient R =>
          m (class_of R a) = u ->
          m q = u -> class_of R a = q)
         (related_classes_eq R H0)
         (fun (p : m (class_of R a) = u)
            (p' : m (class_of R x0) = u) =>
          related_classes_eq R (is_ker a x0 (p @ p'^))))
      (fun (p : m (class_of R a) = u)
         (p' : m (class_of R y0) = u) =>
       related_classes_eq R (is_ker a y0 (p @ p'^)))))
  y intros; apply path_ishprop. }fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
H: forall x y : C, m x = u -> m y = u -> x = y
forall x y : hfiber m u, x = y
      intros [x p] [y p'].fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
H: forall x y : C, m x = u -> m y = u -> x = y
x: C
p: m x = u
y: C
p': m y = u
(x; p) = (y; p')
      apply path_sigma_hprop; simpl.fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
u: B
H: forall x y : C, m x = u -> m y = u -> x = y
x: C
p: m x = u
y: C
p': m y = u
x = y
      exact (H x y p p').
    -fs: Funext
A, B: Type
IsHSet0: IsHSet B
f: A -> B
R: Relation A
sR: is_mere_relation A R
is_ker: forall x y : A, f x = f y <~> R x y
C:= quotient R: Type
X: IsHSet C
e:= class_of R: A -> quotient R
m:= quotient_ind R (fun _ : quotient R => B) f
  (fun (x y : A) (H : R x y) =>
   transport_const (related_classes_eq R H) (f x) @
   (is_ker x y)^-1 H): C -> B
f = (fun x : A => m (e x)) reflexivity.
  Defined.

End Kernel.