Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* File Eqdep.v created by Christine Paulin-Mohring in Coq V5.6, May 1992 *)
(* Further documentation and variants of eq_rect_eq by Hugo Herbelin,
   Apr 2003 *)
(* Abstraction with respect to the eq_rect_eq axiom and renaming to
   EqdepFacts.v by Hugo Herbelin, Mar 2006 *)

This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives the consequence of axiomatizing the invariance by substitution of reflexive equality proofs and shows the equivalence between the 4 following statements

Invariance by Substitution of Reflexive Equality Proofs.
Injectivity of Dependent Equality
Uniqueness of Identity Proofs
Uniqueness of Reflexive Identity Proofs
Streicher's Axiom K

These statements are independent of the calculus of constructions 2.

References:

1 T. Streicher, Semantical Investigations into Intensional Type Theory, Habilitationsschrift, LMU München, 1993. 2 M. Hofmann, T. Streicher, The groupoid interpretation of type theory, Proceedings of the meeting Twenty-five years of constructive type theory, Venice, Oxford University Press, 1998

Table of contents:

1. Definition of dependent equality and equivalence with equality of dependent pairs and with dependent pair of equalities

2. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K

3. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq

(************************************************************************)

Definition of dependent equality and equivalence with equality of dependent pairs

Import EqNotations.

(* Set Universe Polymorphism. *)

Section Dependent_Equality.

  Variable U : Type.
  Variable P : U -> Type.

Dependent equality

  Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop :=
    eq_dep_intro : eq_dep p x p x.
  Hint Constructors eq_dep: core.

  Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x.U:Type
P:U -> Type
forall (p : U) (x : P p), eq_dep p x p x
  Proof eq_dep_intro.

  Lemma eq_dep_sym :
    forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep q y p x.U:Type
P:U -> Type
forall (p q : U) (x : P p) (y : P q),
eq_dep p x q y -> eq_dep q y p x
  Proof.U:Type
P:U -> Type
forall (p q : U) (x : P p) (y : P q),
eq_dep p x q y -> eq_dep q y p x
    destruct 1; auto.
  Qed.
  Hint Immediate eq_dep_sym: core.

  Lemma eq_dep_trans :
    forall (p q r:U) (x:P p) (y:P q) (z:P r),
      eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z.U:Type
P:U -> Type
forall (p q r : U) (x : P p) (y : P q) (z : P r),
eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z
  Proof.U:Type
P:U -> Type
forall (p q r : U) (x : P p) (y : P q) (z : P r),
eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z
    destruct 1; auto.
  Qed.

  Scheme eq_indd := Induction for eq Sort Prop.

Equivalent definition of dependent equality as a dependent pair of equalities

  Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop :=
    eq_dep1_intro : forall h:q = p, x = rew h in y -> eq_dep1 p x q y.

  Lemma eq_dep1_dep :
    forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y.U:Type
P:U -> Type
forall (p : U) (x : P p) (q : U) (y : P q),
eq_dep1 p x q y -> eq_dep p x q y
  Proof.U:Type
P:U -> Type
forall (p : U) (x : P p) (q : U) (y : P q),
eq_dep1 p x q y -> eq_dep p x q y
    destruct 1 as (eq_qp, H).U:Type
P:U -> Type
p:U
x:P p
q:U
y:P q
eq_qp:q = p
H:x = rew [P] eq_qp in y
eq_dep p x q y
    destruct eq_qp using eq_indd.U:Type
P:U -> Type
q:U
x, y:P q
H:x = rew [P] eq_refl in y
eq_dep q x q y
    rewrite H.U:Type
P:U -> Type
q:U
x, y:P q
H:x = rew [P] eq_refl in y
eq_dep q (rew [P] eq_refl in y) q y
    apply eq_dep_intro.
  Qed.

  Lemma eq_dep_dep1 :
    forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y.U:Type
P:U -> Type
forall (p q : U) (x : P p) (y : P q),
eq_dep p x q y -> eq_dep1 p x q y
  Proof.U:Type
P:U -> Type
forall (p q : U) (x : P p) (y : P q),
eq_dep p x q y -> eq_dep1 p x q y
    destruct 1.U:Type
P:U -> Type
p:U
x:P p
eq_dep1 p x p x
    apply eq_dep1_intro with (eq_refl p).U:Type
P:U -> Type
p:U
x:P p
x = rew [P] eq_refl in x
    simpl; trivial.
  Qed.

End Dependent_Equality.

Arguments eq_dep  [U P] p x q _.
Arguments eq_dep1 [U P] p x q y.

Dependent equality is equivalent to equality on dependent pairs

Lemma eq_sigT_eq_dep :
  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
    existT P p x = existT P q y -> eq_dep p x q y.forall (U : Type) (P : U -> Type) (p q : U) (x : P p)
  (y : P q),
existT P p x = existT P q y -> eq_dep p x q y
Proof.forall (U : Type) (P : U -> Type) (p q : U) (x : P p)
  (y : P q),
existT P p x = existT P q y -> eq_dep p x q y
  intros.U:Type
P:U -> Type
p, q:U
x:P p
y:P q
H:existT P p x = existT P q y
eq_dep p x q y
  dependent rewrite H.U:Type
P:U -> Type
p, q:U
x:P p
y:P q
H:existT P p x = existT P q y
eq_dep q y q y
  apply eq_dep_intro.
Qed.

Lemma eq_dep_eq_sigT :
  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
    eq_dep p x q y -> existT P p x = existT P q y.forall (U : Type) (P : U -> Type) (p q : U) (x : P p)
  (y : P q),
eq_dep p x q y -> existT P p x = existT P q y
Proof.forall (U : Type) (P : U -> Type) (p q : U) (x : P p)
  (y : P q),
eq_dep p x q y -> existT P p x = existT P q y
  destruct 1; reflexivity.
Qed.

Lemma eq_sigT_iff_eq_dep :
  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
    existT P p x = existT P q y <-> eq_dep p x q y.forall (U : Type) (P : U -> Type) (p q : U) (x : P p)
  (y : P q),
existT P p x = existT P q y <-> eq_dep p x q y
Proof.forall (U : Type) (P : U -> Type) (p q : U) (x : P p)
  (y : P q),
existT P p x = existT P q y <-> eq_dep p x q y
  split; auto using eq_sigT_eq_dep, eq_dep_eq_sigT.
Qed.

Notation equiv_eqex_eqdep := eq_sigT_iff_eq_dep (only parsing). (* Compat *)

Lemma eq_sig_eq_dep :
  forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
    exist P p x = exist P q y -> eq_dep p x q y.forall (U : Type) (P : U -> Prop) (p q : U) (x : P p)
  (y : P q),
exist P p x = exist P q y -> eq_dep p x q y
Proof.forall (U : Type) (P : U -> Prop) (p q : U) (x : P p)
  (y : P q),
exist P p x = exist P q y -> eq_dep p x q y
  intros.U:Type
P:U -> Prop
p, q:U
x:P p
y:P q
H:exist P p x = exist P q y
eq_dep p x q y
  dependent rewrite H.U:Type
P:U -> Prop
p, q:U
x:P p
y:P q
H:exist P p x = exist P q y
eq_dep q y q y
  apply eq_dep_intro.
Qed.

Lemma eq_dep_eq_sig :
  forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
    eq_dep p x q y -> exist P p x = exist P q y.forall (U : Type) (P : U -> Prop) (p q : U) (x : P p)
  (y : P q),
eq_dep p x q y -> exist P p x = exist P q y
Proof.forall (U : Type) (P : U -> Prop) (p q : U) (x : P p)
  (y : P q),
eq_dep p x q y -> exist P p x = exist P q y
  destruct 1; reflexivity.
Qed.

Lemma eq_sig_iff_eq_dep :
  forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
    exist P p x = exist P q y <-> eq_dep p x q y.forall (U : Type) (P : U -> Prop) (p q : U) (x : P p)
  (y : P q),
exist P p x = exist P q y <-> eq_dep p x q y
Proof.forall (U : Type) (P : U -> Prop) (p q : U) (x : P p)
  (y : P q),
exist P p x = exist P q y <-> eq_dep p x q y
  split; auto using eq_sig_eq_dep, eq_dep_eq_sig.
Qed.

Dependent equality is equivalent to a dependent pair of equalities

Set Implicit Arguments.

Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <->
                                                   {H:x1=x2 | rew H in H1 = H2}.forall (X : Type) (P : X -> Type) (x1 x2 : X)
  (H1 : P x1) (H2 : P x2),
existT P x1 H1 = existT P x2 H2 <->
{H : x1 = x2 | rew [P] H in H1 = H2}
Proof.forall (X : Type) (P : X -> Type) (x1 x2 : X)
  (H1 : P x1) (H2 : P x2),
existT P x1 H1 = existT P x2 H2 <->
{H : x1 = x2 | rew [P] H in H1 = H2}
  intros; split; intro H.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:existT P x1 H1 = existT P x2 H2
{H0 : x1 = x2 | rew [P] H0 in H1 = H2}
X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:{H0 : x1 = x2 | rew [P] H0 in H1 = H2}
existT P x1 H1 = existT P x2 H2
  -X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:existT P x1 H1 = existT P x2 H2
{H0 : x1 = x2 | rew [P] H0 in H1 = H2} change x2 with (projT1 (existT P x2 H2)).X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:existT P x1 H1 = existT P x2 H2
{H0 : x1 = projT1 (existT P x2 H2) |
rew [P] H0 in H1 = H2}
    change H2 with (projT2 (existT P x2 H2)) at 5.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:existT P x1 H1 = existT P x2 H2
{H0 : x1 = projT1 (existT P x2 H2) |
rew [P] H0 in H1 = projT2 (existT P x2 H2)}
    destruct H.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
{H : x1 = projT1 (existT P x1 H1) |
rew [P] H in H1 = projT2 (existT P x1 H1)} simpl.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
{H : x1 = x1 | rew [P] H in H1 = H1}
    exists eq_refl.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
rew [P] eq_refl in H1 = H1
    reflexivity.
  -X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:{H0 : x1 = x2 | rew [P] H0 in H1 = H2}
existT P x1 H1 = existT P x2 H2 destruct H as (->,<-).X:Type
P:X -> Type
x2:X
H1:P x2
existT P x2 H1 = existT P x2 (rew [P] eq_refl in H1)
    reflexivity.
Defined.

Lemma eq_sigT_fst :
  forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), x1 = x2.forall (X : Type) (P : X -> Type) (x1 x2 : X)
  (H1 : P x1) (H2 : P x2),
existT P x1 H1 = existT P x2 H2 -> x1 = x2
Proof.forall (X : Type) (P : X -> Type) (x1 x2 : X)
  (H1 : P x1) (H2 : P x2),
existT P x1 H1 = existT P x2 H2 -> x1 = x2
  intros.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:existT P x1 H1 = existT P x2 H2
x1 = x2
  change x2 with (projT1 (existT P x2 H2)).X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:existT P x1 H1 = existT P x2 H2
x1 = projT1 (existT P x2 H2)
  destruct H.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
x1 = projT1 (existT P x1 H1)
  reflexivity.
Defined.

Lemma eq_sigT_snd :
  forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2.forall (X : Type) (P : X -> Type) (x1 x2 : X)
  (H1 : P x1) (H2 : P x2)
  (H : existT P x1 H1 = existT P x2 H2),
rew [P] eq_sigT_fst H in H1 = H2
Proof.forall (X : Type) (P : X -> Type) (x1 x2 : X)
  (H1 : P x1) (H2 : P x2)
  (H : existT P x1 H1 = existT P x2 H2),
rew [P] eq_sigT_fst H in H1 = H2
  intros.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:existT P x1 H1 = existT P x2 H2
rew [P] eq_sigT_fst H in H1 = H2
  unfold eq_sigT_fst.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:existT P x1 H1 = existT P x2 H2
rew [P]
    match H in (_ = y) return (x1 = projT1 y) with
    | eq_refl => eq_refl
    end in H1 = H2
  change x2 with (projT1 (existT P x2 H2)).X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:existT P x1 H1 = existT P x2 H2
rew [P]
    match H in (_ = y) return (x1 = projT1 y) with
    | eq_refl => eq_refl
    end in H1 = H2
  change H2 with (projT2 (existT P x2 H2)) at 3.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
H:existT P x1 H1 = existT P x2 H2
rew [P]
    match H in (_ = y) return (x1 = projT1 y) with
    | eq_refl => eq_refl
    end in H1 = projT2 (existT P x2 H2)
  destruct H.X:Type
P:X -> Type
x1, x2:X
H1:P x1
H2:P x2
rew [P] eq_refl in H1 = projT2 (existT P x1 H1)
  reflexivity.
Defined.

Lemma eq_sig_fst :
  forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), x1 = x2.forall (X : Type) (P : X -> Prop) (x1 x2 : X)
  (H1 : P x1) (H2 : P x2),
exist P x1 H1 = exist P x2 H2 -> x1 = x2
Proof.forall (X : Type) (P : X -> Prop) (x1 x2 : X)
  (H1 : P x1) (H2 : P x2),
exist P x1 H1 = exist P x2 H2 -> x1 = x2
  intros.X:Type
P:X -> Prop
x1, x2:X
H1:P x1
H2:P x2
H:exist P x1 H1 = exist P x2 H2
x1 = x2
  change x2 with (proj1_sig (exist P x2 H2)).X:Type
P:X -> Prop
x1, x2:X
H1:P x1
H2:P x2
H:exist P x1 H1 = exist P x2 H2
x1 = proj1_sig (exist P x2 H2)
  destruct H.X:Type
P:X -> Prop
x1, x2:X
H1:P x1
H2:P x2
x1 = proj1_sig (exist P x1 H1)
  reflexivity.
Defined.

Lemma eq_sig_snd :
  forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), rew (eq_sig_fst H) in H1 = H2.forall (X : Type) (P : X -> Prop) (x1 x2 : X)
  (H1 : P x1) (H2 : P x2)
  (H : exist P x1 H1 = exist P x2 H2),
rew [P] eq_sig_fst H in H1 = H2
Proof.forall (X : Type) (P : X -> Prop) (x1 x2 : X)
  (H1 : P x1) (H2 : P x2)
  (H : exist P x1 H1 = exist P x2 H2),
rew [P] eq_sig_fst H in H1 = H2
  intros.X:Type
P:X -> Prop
x1, x2:X
H1:P x1
H2:P x2
H:exist P x1 H1 = exist P x2 H2
rew [P] eq_sig_fst H in H1 = H2
  unfold eq_sig_fst, eq_ind.X:Type
P:X -> Prop
x1, x2:X
H1:P x1
H2:P x2
H:exist P x1 H1 = exist P x2 H2
rew [P]
    match H in (_ = y) return (x1 = proj1_sig y) with
    | eq_refl => eq_refl
    end in H1 = H2
  change x2 with (proj1_sig (exist P x2 H2)).X:Type
P:X -> Prop
x1, x2:X
H1:P x1
H2:P x2
H:exist P x1 H1 = exist P x2 H2
rew [P]
    match H in (_ = y) return (x1 = proj1_sig y) with
    | eq_refl => eq_refl
    end in H1 = H2
  change H2 with (proj2_sig (exist P x2 H2)) at 3.X:Type
P:X -> Prop
x1, x2:X
H1:P x1
H2:P x2
H:exist P x1 H1 = exist P x2 H2
rew [P]
    match H in (_ = y) return (x1 = proj1_sig y) with
    | eq_refl => eq_refl
    end in H1 = proj2_sig (exist P x2 H2)
  destruct H.X:Type
P:X -> Prop
x1, x2:X
H1:P x1
H2:P x2
rew [P] eq_refl in H1 = proj2_sig (exist P x1 H1)
  reflexivity.
Defined.

Unset Implicit Arguments.

Exported hints

Hint Resolve eq_dep_intro: core.
Hint Immediate eq_dep_sym: core.

(************************************************************************)

Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K

Section Equivalences.

  Variable U:Type.

Invariance by Substitution of Reflexive Equality Proofs

  Definition Eq_rect_eq_on (p : U) (Q : U -> Type) (x : Q p) :=
    forall (h : p = p), x = eq_rect p Q x p h.
  Definition Eq_rect_eq := forall p Q x, Eq_rect_eq_on p Q x.

Injectivity of Dependent Equality

  Definition Eq_dep_eq_on (P : U -> Type) (p : U) (x : P p) :=
    forall (y : P p), eq_dep p x p y -> x = y.
  Definition Eq_dep_eq := forall P p x, Eq_dep_eq_on P p x.

Uniqueness of Identity Proofs (UIP)

  Definition UIP_on_ (x y : U) (p1 : x = y) :=
    forall (p2 : x = y), p1 = p2.
  Definition UIP_ := forall x y p1, UIP_on_ x y p1.

Uniqueness of Reflexive Identity Proofs

  Definition UIP_refl_on_ (x : U) :=
    forall (p : x = x), p = eq_refl x.
  Definition UIP_refl_ := forall x, UIP_refl_on_ x.

Streicher's axiom K

  Definition Streicher_K_on_ (x : U) (P : x = x -> Prop) :=
    P (eq_refl x) -> forall p : x = x, P p.
  Definition Streicher_K_ := forall x P, Streicher_K_on_ x P.

Injectivity of Dependent Equality is a consequence of

Invariance by Substitution of Reflexive Equality Proof

  Lemma eq_rect_eq_on__eq_dep1_eq_on (p : U) (P : U -> Type) (y : P p) :
    Eq_rect_eq_on p P y -> forall (x : P p), eq_dep1 p x p y -> x = y.U:Type
p:U
P:U -> Type
y:P p
Eq_rect_eq_on p P y ->
forall x : P p, eq_dep1 p x p y -> x = y
  Proof.U:Type
p:U
P:U -> Type
y:P p
Eq_rect_eq_on p P y ->
forall x : P p, eq_dep1 p x p y -> x = y
    intro eq_rect_eq.U:Type
p:U
P:U -> Type
y:P p
eq_rect_eq:Eq_rect_eq_on p P y
forall x : P p, eq_dep1 p x p y -> x = y
    simple destruct 1; intro.U:Type
p:U
P:U -> Type
y:P p
eq_rect_eq:Eq_rect_eq_on p P y
x:P p
H:eq_dep1 p x p y
h:p = p
x = rew [P] h in y -> x = y
    rewrite <- eq_rect_eq; auto.
  Qed.
  Lemma eq_rect_eq__eq_dep1_eq :
    Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y.U:Type
Eq_rect_eq ->
forall (P : U -> Type) (p : U) (x y : P p),
eq_dep1 p x p y -> x = y
  Proof (fun eq_rect_eq P p y x =>
           @eq_rect_eq_on__eq_dep1_eq_on p P x (eq_rect_eq p P x) y).

  Lemma eq_rect_eq_on__eq_dep_eq_on (p : U) (P : U -> Type) (x : P p) :
    Eq_rect_eq_on p P x -> Eq_dep_eq_on P p x.U:Type
p:U
P:U -> Type
x:P p
Eq_rect_eq_on p P x -> Eq_dep_eq_on P p x
  Proof.U:Type
p:U
P:U -> Type
x:P p
Eq_rect_eq_on p P x -> Eq_dep_eq_on P p x
    intros eq_rect_eq; red; intros.U:Type
p:U
P:U -> Type
x:P p
eq_rect_eq:Eq_rect_eq_on p P x
y:P p
H:eq_dep p x p y
x = y
    symmetry; apply (eq_rect_eq_on__eq_dep1_eq_on _ _ _ eq_rect_eq).U:Type
p:U
P:U -> Type
x:P p
eq_rect_eq:Eq_rect_eq_on p P x
y:P p
H:eq_dep p x p y
eq_dep1 p y p x
    apply eq_dep_sym in H; apply eq_dep_dep1; trivial.
  Qed.
  Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.U:Type
Eq_rect_eq -> Eq_dep_eq
  Proof (fun eq_rect_eq P p x y =>
           @eq_rect_eq_on__eq_dep_eq_on p P x (eq_rect_eq p P x) y).

Uniqueness of Identity Proofs (UIP) is a consequence of

Injectivity of Dependent Equality

  Lemma eq_dep_eq_on__UIP_on (x y : U) (p1 : x = y) :
    Eq_dep_eq_on (fun y => x = y) x eq_refl -> UIP_on_ x y p1.U:Type
x, y:U
p1:x = y
Eq_dep_eq_on (fun y0 : U => x = y0) x eq_refl ->
UIP_on_ x y p1
  Proof.U:Type
x, y:U
p1:x = y
Eq_dep_eq_on (fun y0 : U => x = y0) x eq_refl ->
UIP_on_ x y p1
    intro eq_dep_eq; red.U:Type
x, y:U
p1:x = y
eq_dep_eq:Eq_dep_eq_on (fun y0 : U => x = y0) x
  eq_refl
forall p2 : x = y, p1 = p2
    elim p1 using eq_indd.U:Type
x, y:U
p1:x = y
eq_dep_eq:Eq_dep_eq_on (fun y0 : U => x = y0) x
  eq_refl
forall p2 : x = x, eq_refl = p2
    intros; apply eq_dep_eq.U:Type
x, y:U
p1:x = y
eq_dep_eq:Eq_dep_eq_on (fun y0 : U => x = y0) x
  eq_refl
p2:x = x
eq_dep x eq_refl x p2
    elim p2 using eq_indd.U:Type
x, y:U
p1:x = y
eq_dep_eq:Eq_dep_eq_on (fun y0 : U => x = y0) x
  eq_refl
p2:x = x
eq_dep x eq_refl x eq_refl
    apply eq_dep_intro.
  Qed.
  Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_.U:Type
Eq_dep_eq -> UIP_
  Proof (fun eq_dep_eq x y p1 =>
           @eq_dep_eq_on__UIP_on x y p1 (eq_dep_eq _ _ _)).

Uniqueness of Reflexive Identity Proofs is a direct instance of UIP

  Lemma UIP_on__UIP_refl_on (x : U) :
    UIP_on_ x x eq_refl -> UIP_refl_on_ x.U:Type
x:U
UIP_on_ x x eq_refl -> UIP_refl_on_ x
  Proof.U:Type
x:U
UIP_on_ x x eq_refl -> UIP_refl_on_ x
    intro UIP; red; intros; symmetry; apply UIP.
  Qed.
  Lemma UIP__UIP_refl : UIP_ -> UIP_refl_.U:Type
UIP_ -> UIP_refl_
  Proof (fun UIP x p =>
           @UIP_on__UIP_refl_on x (UIP x x eq_refl) p).

Streicher's axiom K is a direct consequence of Uniqueness of Reflexive Identity Proofs

  Lemma UIP_refl_on__Streicher_K_on (x : U) (P : x = x -> Prop) :
    UIP_refl_on_ x -> Streicher_K_on_ x P.U:Type
x:U
P:x = x -> Prop
UIP_refl_on_ x -> Streicher_K_on_ x P
  Proof.U:Type
x:U
P:x = x -> Prop
UIP_refl_on_ x -> Streicher_K_on_ x P
    intro UIP_refl; red; intros; rewrite UIP_refl; assumption.
  Qed.
  Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_.U:Type
UIP_refl_ -> Streicher_K_
  Proof (fun UIP_refl x P =>
           @UIP_refl_on__Streicher_K_on x P (UIP_refl x)).

We finally recover from K the Invariance by Substitution of Reflexive Equality Proofs

  Lemma Streicher_K_on__eq_rect_eq_on (p : U) (P : U -> Type) (x : P p) :
    Streicher_K_on_ p (fun h => x = rew -> [P] h in x)
    -> Eq_rect_eq_on p P x.U:Type
p:U
P:U -> Type
x:P p
Streicher_K_on_ p
  (fun h : p = p => x = rew [P] h in x) ->
Eq_rect_eq_on p P x
  Proof.U:Type
p:U
P:U -> Type
x:P p
Streicher_K_on_ p
  (fun h : p = p => x = rew [P] h in x) ->
Eq_rect_eq_on p P x
    intro Streicher_K; red; intros.U:Type
p:U
P:U -> Type
x:P p
Streicher_K:Streicher_K_on_ p
  (fun h0 : p = p => x = rew [P] h0 in x)
h:p = p
x = rew [P] h in x
    apply Streicher_K.U:Type
p:U
P:U -> Type
x:P p
Streicher_K:Streicher_K_on_ p
  (fun h0 : p = p => x = rew [P] h0 in x)
h:p = p
x = rew [P] eq_refl in x
    reflexivity.
  Qed.
  Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq.U:Type
Streicher_K_ -> Eq_rect_eq
  Proof (fun Streicher_K p P x =>
           @Streicher_K_on__eq_rect_eq_on p P x (Streicher_K p _)).

Remark: It is reasonable to think that eq_rect_eq is strictly stronger than eq_rec_eq (which is eq_rect_eq restricted on Set):

Definition Eq_rec_eq := ∀ (P:U → Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.

Typically, eq_rect_eq allows proving UIP and Streicher's K what does not seem possible with eq_rec_eq. In particular, the proof of UIP requires to use eq_rect_eq on fun y → x=y which is in Type but not in Set.

End Equivalences.

UIP_refl is downward closed (a short proof of the key lemma of Voevodsky's proof of inclusion of h-level n into h-level n+1; see hlevelntosn in https://github.com/vladimirias/Foundations.git).

Theorem UIP_shift_on (X : Type) (x : X) :
  UIP_refl_on_ X x -> forall y : x = x, UIP_refl_on_ (x = x) y.X:Type
x:X
UIP_refl_on_ X x ->
forall y : x = x, UIP_refl_on_ (x = x) y
Proof.X:Type
x:X
UIP_refl_on_ X x ->
forall y : x = x, UIP_refl_on_ (x = x) y
  intros UIP_refl y.X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
UIP_refl_on_ (x = x) y
  rewrite (UIP_refl y).X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
UIP_refl_on_ (x = x) eq_refl
  intros z.X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
z = eq_refl
  assert (UIP:forall y' y'' : x = x, y' = y'').X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
forall y' y'' : x = x, y' = y''
X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
UIP:forall y' y'' : x = x, y' = y''
z = eq_refl
  {X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
forall y' y'' : x = x, y' = y'' intros.X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
y', y'':x = x
y' = y'' apply eq_trans_r with (eq_refl x); apply UIP_refl. }X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
UIP:forall y' y'' : x = x, y' = y''
z = eq_refl
  transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z)
                         (eq_sym (UIP (eq_refl x) (eq_refl x)))).X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
UIP:forall y' y'' : x = x, y' = y''
z =
eq_trans (eq_trans (UIP eq_refl eq_refl) z)
  (eq_sym (UIP eq_refl eq_refl))
X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
UIP:forall y' y'' : x = x, y' = y''
eq_trans (eq_trans (UIP eq_refl eq_refl) z)
  (eq_sym (UIP eq_refl eq_refl)) = eq_refl
  -X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
UIP:forall y' y'' : x = x, y' = y''
z =
eq_trans (eq_trans (UIP eq_refl eq_refl) z)
  (eq_sym (UIP eq_refl eq_refl)) destruct z.X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
UIP:forall y' y'' : x = x, y' = y''
eq_refl =
eq_trans (eq_trans (UIP eq_refl eq_refl) eq_refl)
  (eq_sym (UIP eq_refl eq_refl)) destruct (UIP _ _).X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
UIP:forall y' y'' : x = x, y' = y''
eq_refl =
eq_trans (eq_trans eq_refl eq_refl) (eq_sym eq_refl) reflexivity.
  -X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
UIP:forall y' y'' : x = x, y' = y''
eq_trans (eq_trans (UIP eq_refl eq_refl) z)
  (eq_sym (UIP eq_refl eq_refl)) = eq_refl change
      (match eq_refl x as y' in _ = x' return y' = y' -> Prop with
       | eq_refl => fun z => z = (eq_refl (eq_refl x))
       end (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z)
                     (eq_sym (UIP (eq_refl x) (eq_refl x))))).X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
z:eq_refl = eq_refl
UIP:forall y' y'' : x = x, y' = y''
match
  eq_refl as y' in (_ = x') return (y' = y' -> Prop)
with
| eq_refl =>
    fun z0 : eq_refl = eq_refl => z0 = eq_refl
end
  (eq_trans (eq_trans (UIP eq_refl eq_refl) z)
     (eq_sym (UIP eq_refl eq_refl)))
    destruct z.X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
UIP:forall y' y'' : x = x, y' = y''
eq_trans (eq_trans (UIP eq_refl eq_refl) eq_refl)
  (eq_sym (UIP eq_refl eq_refl)) = eq_refl destruct (UIP _ _).X:Type
x:X
UIP_refl:UIP_refl_on_ X x
y:x = x
UIP:forall y' y'' : x = x, y' = y''
eq_trans (eq_trans eq_refl eq_refl) (eq_sym eq_refl) =
eq_refl reflexivity.
Qed.
Theorem UIP_shift : forall U, UIP_refl_ U -> forall x:U, UIP_refl_ (x = x).forall U : Type,
UIP_refl_ U -> forall x : U, UIP_refl_ (x = x)
Proof (fun U UIP_refl x =>
         @UIP_shift_on U x (UIP_refl x)).

Section Corollaries.

  Variable U:Type.

UIP implies the injectivity of equality on dependent pairs in Type

 Definition Inj_dep_pair_on (P : U -> Type) (p : U) (x : P p) :=
   forall (y : P p), existT P p x = existT P p y -> x = y.
 Definition Inj_dep_pair := forall P p x, Inj_dep_pair_on P p x.

 Lemma eq_dep_eq_on__inj_pair2_on (P : U -> Type) (p : U) (x : P p) :
   Eq_dep_eq_on U P p x -> Inj_dep_pair_on P p x.U:Type
P:U -> Type
p:U
x:P p
Eq_dep_eq_on U P p x -> Inj_dep_pair_on P p x
 Proof.U:Type
P:U -> Type
p:U
x:P p
Eq_dep_eq_on U P p x -> Inj_dep_pair_on P p x
   intro eq_dep_eq; red; intros.U:Type
P:U -> Type
p:U
x:P p
eq_dep_eq:Eq_dep_eq_on U P p x
y:P p
H:existT P p x = existT P p y
x = y
   apply eq_dep_eq.U:Type
P:U -> Type
p:U
x:P p
eq_dep_eq:Eq_dep_eq_on U P p x
y:P p
H:existT P p x = existT P p y
eq_dep p x p y
   apply eq_sigT_eq_dep.U:Type
P:U -> Type
p:U
x:P p
eq_dep_eq:Eq_dep_eq_on U P p x
y:P p
H:existT P p x = existT P p y
existT P p x = existT P p y
   assumption.
 Qed.
 Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair.U:Type
Eq_dep_eq U -> Inj_dep_pair
 Proof (fun eq_dep_eq P p x =>
          @eq_dep_eq_on__inj_pair2_on P p x (eq_dep_eq P p x)).

End Corollaries.

Notation Inj_dep_pairS := Inj_dep_pair.
Notation Inj_dep_pairT := Inj_dep_pair.
Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2.


(************************************************************************)

Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq

Module Type EqdepElimination.

  Axiom eq_rect_eq :
    forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p),
      x = eq_rect p Q x p h.

End EqdepElimination.

Module EqdepTheory (M:EqdepElimination).

  Section Axioms.

    Variable U:Type.

Invariance by Substitution of Reflexive Equality Proofs

Lemma eq_rect_eq :
  forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.U:Type
forall (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
x = rew [Q] h in x
Proof M.eq_rect_eq U.

Lemma eq_rec_eq :
  forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h.U:Type
forall (p : U) (Q : U -> Set) (x : Q p) (h : p = p),
x = eq_rec p Q x p h
Proof (fun p Q => M.eq_rect_eq U p Q).

Injectivity of Dependent Equality

Lemma eq_dep_eq : forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y.U:Type
forall (P : U -> Type) (p : U) (x y : P p),
eq_dep p x p y -> x = y
Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).

Uniqueness of Identity Proofs (UIP) is a consequence of

Injectivity of Dependent Equality

Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.U:Type
forall (x y : U) (p1 p2 : x = y), p1 = p2
Proof (eq_dep_eq__UIP U eq_dep_eq).

Uniqueness of Reflexive Identity Proofs is a direct instance of UIP

Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x.U:Type
forall (x : U) (p : x = x), p = eq_refl
Proof (UIP__UIP_refl U UIP).

Streicher's axiom K is a direct consequence of Uniqueness of Reflexive Identity Proofs

Lemma Streicher_K :
  forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.U:Type
forall (x : U) (P : x = x -> Prop),
P eq_refl -> forall p : x = x, P p
Proof (UIP_refl__Streicher_K U UIP_refl).

End Axioms.

UIP implies the injectivity of equality on dependent pairs in Type

Lemma inj_pair2 :
 forall (U:Type) (P:U -> Type) (p:U) (x y:P p),
   existT P p x = existT P p y -> x = y.forall (U : Type) (P : U -> Type) (p : U) (x y : P p),
existT P p x = existT P p y -> x = y
Proof (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)).

Notation inj_pairT2 := inj_pair2.

End EqdepTheory.

Basic facts about eq_dep

Lemma f_eq_dep :
  forall U (P:U->Type) R p q x y (f:forall p, P p -> R p),
    eq_dep p x q y -> eq_dep p (f p x) q (f q y).forall (U : Type) (P R : U -> Type) (p q : U)
  (x : P p) (y : P q)
  (f : forall p0 : U, P p0 -> R p0),
eq_dep p x q y -> eq_dep p (f p x) q (f q y)
Proof.forall (U : Type) (P R : U -> Type) (p q : U)
  (x : P p) (y : P q)
  (f : forall p0 : U, P p0 -> R p0),
eq_dep p x q y -> eq_dep p (f p x) q (f q y)
intros * [].U:Type
P, R:U -> Type
p, q:U
x:P p
y:P q
f:forall p0 : U, P p0 -> R p0
eq_dep p (f p x) p (f p x) reflexivity.
Qed.

Lemma eq_dep_non_dep :
  forall U P p q x y, @eq_dep U (fun _ => P) p x q y -> x = y.forall (U P : Type) (p q : U) (x y : P),
eq_dep p x q y -> x = y
Proof.forall (U P : Type) (p q : U) (x y : P),
eq_dep p x q y -> x = y
intros * [].U, P:Type
p, q:U
x, y:P
x = x reflexivity.
Qed.

Lemma f_eq_dep_non_dep :
  forall U (P:U->Type) R p q x y (f:forall p, P p -> R),
    eq_dep p x q y -> f p x = f q y.forall (U : Type) (P : U -> Type) (R : Type) (p q : U)
  (x : P p) (y : P q) (f : forall p0 : U, P p0 -> R),
eq_dep p x q y -> f p x = f q y
Proof.forall (U : Type) (P : U -> Type) (R : Type) (p q : U)
  (x : P p) (y : P q) (f : forall p0 : U, P p0 -> R),
eq_dep p x q y -> f p x = f q y
intros * [].U:Type
P:U -> Type
R:Type
p, q:U
x:P p
y:P q
f:forall p0 : U, P p0 -> R
f p x = f p x reflexivity.
Qed.

Arguments eq_dep  U P p x q _ : clear implicits.
Arguments eq_dep1 U P p x q y : clear implicits.