Facts stating equivalence of axioms K, URIP, UIP, eq_rect_eq, projT_2_eq and JMeq_eq in Coq.

EqFacts.v

Require Import Coq.Logic.JMeq.

Definition JMeq_eq := forall (A : Type) (x y : A), JMeq x y -> x = y.

Section Eq_Facts.
  Variable A : Type.

  Definition K := forall (x : A) (P : x = x -> Prop), P eq_refl -> forall (eq : x = x), P eq.

  Definition URIP := forall (x : A) (eq : x = x), eq = eq_refl.

  Definition UIP := forall (x y : A) (eq eq' : x = y), eq = eq'.

  Definition eq_rect_eq := forall (x : A) (P : A -> Type) (eq : x = x) (p : P x), p = eq_rect x P p x eq.

  Definition projT2_eq := forall (x : A) (P : A -> Type) (p q : P x), existT P x p = existT P x q -> p = q.

  Lemma K_URIP : K -> URIP.
  Proof.
    intros k x eq. 
    apply (k _ (fun p => p = eq_refl) eq_refl).
  Qed.

  Lemma UIP_UIP : URIP -> UIP.
  Proof.
    intros urip x y eq eq'. 
    destruct eq'.
    apply urip.
  Qed.

  Theorem UIP_eq_rect_eq : UIP -> eq_rect_eq.
  Proof.
    intros uip x P eq p.
    rewrite (uip _ _ eq eq_refl); trivial.
  Qed.    

  Theorem eq_rect_eq_projT2_eq : eq_rect_eq -> projT2_eq.
  Proof.
    intros ere x P p q H.
    set (proj1_eq := fun (v : sigT P) (H : existT P x p = v) => match H in _ = z return projT1 (existT P x p) = projT1 z with eq_refl => eq_refl end).
    assert (H' : match (proj1_eq (existT P x q) H) in _ = u return P u with eq_refl => projT2 (existT P x p) end = projT2 (existT P x q)).
    {
      destruct H; trivial.
    }
    cbv in ere.
    rewrite <- (ere _ _ (proj1_eq _ H)) in H'; trivial.
  Qed.    

  Theorem projT2_eq_k : projT2_eq -> K.
  Proof.
    intros p2 x P H eq.
    cut (eq = eq_refl); [intros H'; rewrite H'; trivial|].
    apply p2; destruct eq; trivial.
  Qed.

  Section Dec.
    Hypothesis A_dec : forall a b : A, {a = b} + {a <> b}.

    Definition make_eq {a b : A} (eq : a = b) : a = b.
    Proof.
      destruct (A_dec a b) as [H|H].
      + exact H.
      + exact (False_rect _ (H eq)).
    Defined.

    Theorem make_eq_const : forall {a b : A} (eq eq' : a = b), make_eq eq = make_eq eq'.
    Proof.
      intros a b eq eq'.
      cbv.
      destruct A_dec as [H|H]; trivial.
      destruct (H eq).
    Qed.

    Theorem make_eq_com_sym : forall {a b : A} (eq : a = b), eq_trans (eq_sym (make_eq (eq_refl a))) (make_eq eq) = eq.
    Proof.
      intros a b eq.
      destruct eq.
      destruct (make_eq eq_refl); trivial.
    Qed.    

    Theorem k : K.
    Proof.
      intros x P H eq.
      rewrite <- make_eq_com_sym in H.
      rewrite <- make_eq_com_sym.
      replace (make_eq eq) with (make_eq (eq_refl x)); trivial.
      apply make_eq_const.
    Qed.
  End Dec.
End Eq_Facts.

Theorem projT2_eq_JMeq_eq : (forall A, projT2_eq A) <-> JMeq_eq.
  Proof.
    split.
    {
      intros p2 A x y H.
      inversion H as [H1 H2].
      exact (p2 Type _ _ _ _ H2).
    }
    {
      intros je A x P p q H.
      apply je.
      change (JMeq (projT2 (existT P x p)) (projT2 (existT P x q))).
      rewrite H.
      exact JMeq_refl.
    }
  Qed.