(*|
商型
==========

商などを定義する。
|*)

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 (* .unfold *).
Check propositional_extensionality (* .unfold *).
Check proof_irrelevance (* .unfold *).

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.
  Proof.
    intros.
    extensionality c.
    apply propositional_extensionality.
    split.
    -
      intro.
      eapply (trans A (proj1_sig R)).
      +
        exact (proj2_sig R).
      +
        apply sym.
        exact (proj2_sig R).
        exact H.
      +
        assumption.
    -
      intro.
      eapply (trans A (proj1_sig R)).
      +
        exact (proj2_sig R).
      +
        exact H.
      +
        assumption.
  Qed.

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

  Definition quot_map (a : A) : quot A R.
  Proof.
    exists (eq_class R a).
    econstructor.
    reflexivity.
  Defined.

  Print quot_map.

  Lemma quot_map_respect_rel : forall a b,
    proj1_sig R a b
    -> quot_map a = quot_map b.
  Proof.
    intros.
    apply (
      eq_sig
        (quot_map a)
        (quot_map b)
        (related_same_eq_class a b H)
    ).
    apply proof_irrelevance.
  Qed.

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

  Lemma quot_map_surjective : surjective quot_map.
  Proof.
    unfold surjective.
    intros.
    destruct b as [c [a r]].
    rewrite r.
    exists a.
    unshelve eapply eq_sig.
    -
      reflexivity.
    -
      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.
    Proof.
      intro.
      destruct x as [c [a e]].
      exists (f a).
      split.
      -
        exists a.
        simpl.
        auto.
      -
        simpl.
        intros.
        destruct H as [a' [v v']].
        rewrite<- v'.
        apply (f_preserve_R_to_eq a a').
        subst c.
        apply same_eq_class_related.
        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.
    Proof.
      intros.
      destruct (proj2_sig helper2 (quot_map a)) as [x [H H0]].
      fold the_map in H0.
      rewrite<- H0.
      apply f_preserve_R_to_eq.
      apply same_eq_class_related.
      symmetry.
      exact H.
    Qed.

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