商型

商などを定義する。

Require Import function.
Require Import unique_choice.
Require Import power.
Require Import relation.
From Stdlib Require Import Logic.FunctionalExtensionality.
From Stdlib Require Import Logic.PropExtensionality.
From Stdlib Require Import Logic.ProofIrrelevance.

同値関係

Record is_eq_rel (A : Type) (R : bin_rel A) : Prop := mk_is_eq_rel
  { ref : forall x, R x x
  ; sym : forall x y, R x y -> R y x
  ; trans : forall x y z, R x y -> R y z -> R x z
  }.

Definition eq_rel (A : Type) : Type :=
  { R : bin_rel A | is_eq_rel A R }.

同値類

Definition eq_class (A : Type) (R : eq_rel A) (x : A) : power A :=
  fun y => proj1_sig R x y.

Arguments eq_class {_}.

商型

Definition quot (A : Type) (R : eq_rel A) : Type :=
  { c : power A | exists b : A, c = eq_class R b }.

Check @functional_extensionality.@functional_extensionality
     : forall (A B : Type) (f g : A -> B), (forall x : A, f x = g x) -> f = g
Check propositional_extensionality.propositional_extensionality
     : forall P Q : Prop, P <-> Q -> P = Q
Check proof_irrelevance.proof_irrelevance
     : forall (P : Prop) (p1 p2 : P), p1 = p2

Section Quotients.
  Variable A : Type.
  Variable R : eq_rel A.

  Lemma related_same_eq_class : forall a b,
    proj1_sig R a b
    -> eq_class R a = eq_class R b.A: Type
R: eq_rel A
forall a b : A, proj1_sig R a b -> eq_class R a = eq_class R b
  Proof.A: Type
R: eq_rel A
forall a b : A, proj1_sig R a b -> eq_class R a = eq_class R b
    intros.A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
eq_class R a = eq_class R b
    extensionality c.A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
eq_class R a c = eq_class R b c
    apply propositional_extensionality.A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
eq_class R a c <-> eq_class R b c
    split.A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
eq_class R a c -> eq_class R b c
A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
eq_class R b c -> eq_class R a c
    -A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
eq_class R a c -> eq_class R b c
      intro.A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R a c
eq_class R b c
      eapply (trans A (proj1_sig R)).A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R a c
is_eq_rel A (proj1_sig R)
A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R a c
proj1_sig R b ?y
A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R a c
proj1_sig R ?y c
      +A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R a c
is_eq_rel A (proj1_sig R)
        exact (proj2_sig R).
      +A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R a c
proj1_sig R b ?y
        apply sym.A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R a c
is_eq_rel A (proj1_sig R)
A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R a c
proj1_sig R ?y b
        exact (proj2_sig R).A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R a c
proj1_sig R ?y b
        exact H.
      +A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R a c
proj1_sig R a c
        assumption.
    -A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
eq_class R b c -> eq_class R a c
      intro.A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R b c
eq_class R a c
      eapply (trans A (proj1_sig R)).A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R b c
is_eq_rel A (proj1_sig R)
A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R b c
proj1_sig R a ?y
A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R b c
proj1_sig R ?y c
      +A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R b c
is_eq_rel A (proj1_sig R)
        exact (proj2_sig R).
      +A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R b c
proj1_sig R a ?y
        exact H.
      +A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
c: A
H0: eq_class R b c
proj1_sig R b c
        assumption.
  Qed.

  Lemma same_eq_class_related : forall a b,
    eq_class R a = eq_class R b
    -> proj1_sig R a b.A: Type
R: eq_rel A
forall a b : A, eq_class R a = eq_class R b -> proj1_sig R a b
  Proof.A: Type
R: eq_rel A
forall a b : A, eq_class R a = eq_class R b -> proj1_sig R a b
    intros.A: Type
R: eq_rel A
a, b: A
H: eq_class R a = eq_class R b
proj1_sig R a b
    assert (H' : eq_class R a b = eq_class R b b).A: Type
R: eq_rel A
a, b: A
H: eq_class R a = eq_class R b
eq_class R a b = eq_class R b b
A: Type
R: eq_rel A
a, b: A
H: eq_class R a = eq_class R b
H': eq_class R a b = eq_class R b b
proj1_sig R a b
    rewrite<- H.A: Type
R: eq_rel A
a, b: A
H: eq_class R a = eq_class R b
eq_class R a b = eq_class R a b
A: Type
R: eq_rel A
a, b: A
H: eq_class R a = eq_class R b
H': eq_class R a b = eq_class R b b
proj1_sig R a b
    reflexivity.A: Type
R: eq_rel A
a, b: A
H: eq_class R a = eq_class R b
H': eq_class R a b = eq_class R b b
proj1_sig R a b
    unfold eq_class in H'.A: Type
R: eq_rel A
a, b: A
H: eq_class R a = eq_class R b
H': proj1_sig R a b = proj1_sig R b b
proj1_sig R a b
    rewrite H'.A: Type
R: eq_rel A
a, b: A
H: eq_class R a = eq_class R b
H': proj1_sig R a b = proj1_sig R b b
proj1_sig R b b
    apply ref.A: Type
R: eq_rel A
a, b: A
H: eq_class R a = eq_class R b
H': proj1_sig R a b = proj1_sig R b b
is_eq_rel A (proj1_sig R)
    exact (proj2_sig R).
  Qed.

  Definition quot_map (a : A) : quot A R.A: Type
R: eq_rel A
a: A
quot A R
  Proof.A: Type
R: eq_rel A
a: A
quot A R
    exists (eq_class R a).A: Type
R: eq_rel A
a: A
exists b : A, eq_class R a = eq_class R b
    econstructor.A: Type
R: eq_rel A
a: A
eq_class R a = eq_class R ?b
    reflexivity.
  Defined.

  Print quot_map.quot_map =
fun a : A =>
exist (fun c : power A => exists b : A, c = eq_class R b) 
  (eq_class R a)
  (ex_intro (fun b : A => eq_class R a = eq_class R b) a eq_refl)
     : A -> quot A R

Arguments quot_map a
quot_map uses section variables A R.

  Lemma quot_map_respect_rel : forall a b,
    proj1_sig R a b
    -> quot_map a = quot_map b.A: Type
R: eq_rel A
forall a b : A, proj1_sig R a b -> quot_map a = quot_map b
  Proof.A: Type
R: eq_rel A
forall a b : A, proj1_sig R a b -> quot_map a = quot_map b
    intros.A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
quot_map a = quot_map b
    apply (
      eq_sig
        (quot_map a)
        (quot_map b)
        (related_same_eq_class a b H)
    ).A: Type
R: eq_rel A
a, b: A
H: proj1_sig R a b
eq_rect (proj1_sig (quot_map a))
  (fun a0 : power A => exists b0 : A, a0 = eq_class R b0)
  (proj2_sig (quot_map a)) (proj1_sig (quot_map b))
  (related_same_eq_class a b H) =
proj2_sig (quot_map b)
    apply proof_irrelevance.
  Qed.

  Theorem effective_quotient :
    forall (a b : A),
    quot_map a = quot_map b
    -> proj1_sig R a b.A: Type
R: eq_rel A
forall a b : A, quot_map a = quot_map b -> proj1_sig R a b
  Proof.A: Type
R: eq_rel A
forall a b : A, quot_map a = quot_map b -> proj1_sig R a b
    intros.A: Type
R: eq_rel A
a, b: A
H: quot_map a = quot_map b
proj1_sig R a b
    apply same_eq_class_related.A: Type
R: eq_rel A
a, b: A
H: quot_map a = quot_map b
eq_class R a = eq_class R b
    assert (H' : proj1_sig (quot_map a) = proj1_sig (quot_map b)).A: Type
R: eq_rel A
a, b: A
H: quot_map a = quot_map b
proj1_sig (quot_map a) = proj1_sig (quot_map b)
A: Type
R: eq_rel A
a, b: A
H: quot_map a = quot_map b
H': proj1_sig (quot_map a) = proj1_sig (quot_map b)
eq_class R a = eq_class R b
    rewrite H.A: Type
R: eq_rel A
a, b: A
H: quot_map a = quot_map b
proj1_sig (quot_map b) = proj1_sig (quot_map b)
A: Type
R: eq_rel A
a, b: A
H: quot_map a = quot_map b
H': proj1_sig (quot_map a) = proj1_sig (quot_map b)
eq_class R a = eq_class R b
    reflexivity.A: Type
R: eq_rel A
a, b: A
H: quot_map a = quot_map b
H': proj1_sig (quot_map a) = proj1_sig (quot_map b)
eq_class R a = eq_class R b
    exact H'.
  Qed.

  Lemma quot_map_surjective : surjective quot_map.A: Type
R: eq_rel A
surjective quot_map
  Proof.A: Type
R: eq_rel A
surjective quot_map
    unfold surjective.A: Type
R: eq_rel A
forall b : quot A R, exists a : A, quot_map a = b
    intros.A: Type
R: eq_rel A
b: quot A R
exists a : A, quot_map a = b
    destruct b as [c [a r]].A: Type
R: eq_rel A
c: power A
a: A
r: c = eq_class R a
exists a0 : A,
  quot_map a0 =
  exist (fun c0 : power A => exists b : A, c0 = eq_class R b) c
    (ex_intro (fun b : A => c = eq_class R b) a r)
    rewrite r.A: Type
R: eq_rel A
c: power A
a: A
r: c = eq_class R a
exists a0 : A,
  quot_map a0 =
  exist (fun c0 : power A => exists b : A, c0 = eq_class R b) 
    (eq_class R a)
    (ex_intro (fun b : A => eq_class R a = eq_class R b) a eq_refl)
    exists a.A: Type
R: eq_rel A
c: power A
a: A
r: c = eq_class R a
quot_map a =
exist (fun c0 : power A => exists b : A, c0 = eq_class R b) 
  (eq_class R a)
  (ex_intro (fun b : A => eq_class R a = eq_class R b) a eq_refl)
    unshelve eapply eq_sig.A: Type
R: eq_rel A
c: power A
a: A
r: c = eq_class R a
proj1_sig (quot_map a) =
proj1_sig
  (exist (fun c0 : power A => exists b : A, c0 = eq_class R b) 
     (eq_class R a)
     (ex_intro (fun b : A => eq_class R a = eq_class R b) a eq_refl))
A: Type
R: eq_rel A
c: power A
a: A
r: c = eq_class R a
eq_rect (proj1_sig (quot_map a))
  (fun a0 : power A => exists b : A, a0 = eq_class R b)
  (proj2_sig (quot_map a))
  (proj1_sig
     (exist (fun c0 : power A => exists b : A, c0 = eq_class R b)
        (eq_class R a)
        (ex_intro (fun b : A => eq_class R a = eq_class R b) a eq_refl)))
  ?p =
proj2_sig
  (exist (fun c0 : power A => exists b : A, c0 = eq_class R b) 
     (eq_class R a)
     (ex_intro (fun b : A => eq_class R a = eq_class R b) a eq_refl))
    -A: Type
R: eq_rel A
c: power A
a: A
r: c = eq_class R a
proj1_sig (quot_map a) =
proj1_sig
  (exist (fun c0 : power A => exists b : A, c0 = eq_class R b) 
     (eq_class R a)
     (ex_intro (fun b : A => eq_class R a = eq_class R b) a eq_refl))
      reflexivity.
    -A: Type
R: eq_rel A
c: power A
a: A
r: c = eq_class R a
eq_rect (proj1_sig (quot_map a))
  (fun a0 : power A => exists b : A, a0 = eq_class R b)
  (proj2_sig (quot_map a))
  (proj1_sig
     (exist (fun c0 : power A => exists b : A, c0 = eq_class R b)
        (eq_class R a)
        (ex_intro (fun b : A => eq_class R a = eq_class R b) a eq_refl)))
  eq_refl =
proj2_sig
  (exist (fun c0 : power A => exists b : A, c0 = eq_class R b) 
     (eq_class R a)
     (ex_intro (fun b : A => eq_class R a = eq_class R b) a eq_refl))
      apply proof_irrelevance.
  Qed.

  Section UniversalProperty.
    Variable B : Type.
    Variable f : A -> B.
    Variable f_preserve_R_to_eq :
      forall x y, proj1_sig R x y -> f x = f y.

    Lemma helper : forall x : quot A R,
      exists! b : B,
      exists a : A,
      proj1_sig x = eq_class R a /\ f a = b.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
forall x : quot A R,
exists ! b : B, exists a : A, proj1_sig x = eq_class R a /\ f a = b
    Proof.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
forall x : quot A R,
exists ! b : B, exists a : A, proj1_sig x = eq_class R a /\ f a = b
      intro.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
x: quot A R
exists ! b : B, exists a : A, proj1_sig x = eq_class R a /\ f a = b
      destruct x as [c [a e]].A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
exists ! b : B,
  exists a0 : A,
    proj1_sig
      (exist (fun c0 : power A => exists b0 : A, c0 = eq_class R b0) c
         (ex_intro (fun b0 : A => c = eq_class R b0) a e)) =
    eq_class R a0 /\ f a0 = b
      exists (f a).A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
unique
  (fun b : B =>
   exists a0 : A,
     proj1_sig
       (exist (fun c0 : power A => exists b0 : A, c0 = eq_class R b0) c
          (ex_intro (fun b0 : A => c = eq_class R b0) a e)) =
     eq_class R a0 /\ f a0 = b)
  (f a)
      split.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
exists a0 : A,
  proj1_sig
    (exist (fun c0 : power A => exists b : A, c0 = eq_class R b) c
       (ex_intro (fun b : A => c = eq_class R b) a e)) =
  eq_class R a0 /\ f a0 = f a
A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
forall x' : B,
(exists a0 : A,
   proj1_sig
     (exist (fun c0 : power A => exists b : A, c0 = eq_class R b) c
        (ex_intro (fun b : A => c = eq_class R b) a e)) =
   eq_class R a0 /\ f a0 = x') ->
f a = x'
      -A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
exists a0 : A,
  proj1_sig
    (exist (fun c0 : power A => exists b : A, c0 = eq_class R b) c
       (ex_intro (fun b : A => c = eq_class R b) a e)) =
  eq_class R a0 /\ f a0 = f a
        exists a.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
proj1_sig
  (exist (fun c0 : power A => exists b : A, c0 = eq_class R b) c
     (ex_intro (fun b : A => c = eq_class R b) a e)) =
eq_class R a /\ f a = f a
        simpl.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
c = eq_class R a /\ f a = f a
        auto.
      -A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
forall x' : B,
(exists a0 : A,
   proj1_sig
     (exist (fun c0 : power A => exists b : A, c0 = eq_class R b) c
        (ex_intro (fun b : A => c = eq_class R b) a e)) =
   eq_class R a0 /\ f a0 = x') ->
f a = x'
        simpl.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
forall x' : B, (exists a0 : A, c = eq_class R a0 /\ f a0 = x') -> f a = x'
        intros.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
x': B
H: exists a : A, c = eq_class R a /\ f a = x'
f a = x'
        destruct H as [a' [v v']].A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
x': B
a': A
v: c = eq_class R a'
v': f a' = x'
f a = x'
        rewrite<- v'.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
x': B
a': A
v: c = eq_class R a'
v': f a' = x'
f a = f a'
        apply (f_preserve_R_to_eq a a').A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
c: power A
a: A
e: c = eq_class R a
x': B
a': A
v: c = eq_class R a'
v': f a' = x'
proj1_sig R a a'
        subst c.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
a: A
x': B
a': A
v: eq_class R a = eq_class R a'
v': f a' = x'
proj1_sig R a a'
        apply same_eq_class_related.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
a: A
x': B
a': A
v: eq_class R a = eq_class R a'
v': f a' = x'
eq_class R a = eq_class R a'
        exact v.
    Qed.

    Definition helper2 :
      { g : quot A R -> B |
        forall x,
        exists a : A,
        proj1_sig x = eq_class R a /\ f a = g x
      } :=
        functional_definite_description
          (quot A R)
          B
          (fun x b =>
            exists a : A, proj1_sig x = eq_class R a /\ f a = b
          )
          helper.

    Definition the_map :
      quot A R -> B
      := proj1_sig helper2.

    Theorem factorize_f :
      forall a : A,
      the_map (quot_map a) = f a.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
forall a : A, the_map (quot_map a) = f a
    Proof.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
forall a : A, the_map (quot_map a) = f a
      intros.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
a: A
the_map (quot_map a) = f a
      destruct (proj2_sig helper2 (quot_map a)) as [x [H H0]].A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
a, x: A
H: proj1_sig (quot_map a) = eq_class R x
H0: f x = proj1_sig helper2 (quot_map a)
the_map (quot_map a) = f a
      fold the_map in H0.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
a, x: A
H: proj1_sig (quot_map a) = eq_class R x
H0: f x = the_map (quot_map a)
the_map (quot_map a) = f a
      rewrite<- H0.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
a, x: A
H: proj1_sig (quot_map a) = eq_class R x
H0: f x = the_map (quot_map a)
f x = f a
      apply f_preserve_R_to_eq.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
a, x: A
H: proj1_sig (quot_map a) = eq_class R x
H0: f x = the_map (quot_map a)
proj1_sig R x a
      apply same_eq_class_related.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
a, x: A
H: proj1_sig (quot_map a) = eq_class R x
H0: f x = the_map (quot_map a)
eq_class R x = eq_class R a
      symmetry.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
a, x: A
H: proj1_sig (quot_map a) = eq_class R x
H0: f x = the_map (quot_map a)
eq_class R a = eq_class R x
      exact H.
    Qed.

    Theorem unique_factorization :
      forall h : quot A R -> B,
      (forall a, h (quot_map a) = f a)
      -> the_map = h.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
forall h : quot A R -> B, (forall a : A, h (quot_map a) = f a) -> the_map = h
    Proof.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
forall h : quot A R -> B, (forall a : A, h (quot_map a) = f a) -> the_map = h
      intros.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
h: quot A R -> B
H: forall a : A, h (quot_map a) = f a
the_map = h
      extensionality c.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
h: quot A R -> B
H: forall a : A, h (quot_map a) = f a
c: quot A R
the_map c = h c
      destruct (quot_map_surjective c) as [a H0].A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
h: quot A R -> B
H: forall a : A, h (quot_map a) = f a
c: quot A R
a: A
H0: quot_map a = c
the_map c = h c
      subst c.A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
h: quot A R -> B
H: forall a : A, h (quot_map a) = f a
a: A
the_map (quot_map a) = h (quot_map a)
      rewrite (H a).A: Type
R: eq_rel A
B: Type
f: A -> B
f_preserve_R_to_eq: forall x y : A, proj1_sig R x y -> f x = f y
h: quot A R -> B
H: forall a : A, h (quot_map a) = f a
a: A
the_map (quot_map a) = f a
      apply factorize_f.
    Qed.
  End UniversalProperty.
End Quotients.