# Library Coq.Logic.EqdepFacts

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
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.

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.
#[local]
Hint Constructors eq_dep: core.

Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x.

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.
#[local]
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.

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.

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.

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.

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.

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.

Notation equiv_eqex_eqdep := eq_sigT_iff_eq_dep (only parsing).
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.

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.

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.

Dependent equality is equivalent to a dependent pair of equalities

Set Implicit Arguments.

Lemma eq_sigT_sig_eq X P (x1 x2:X) H1 H2 :
existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}.

Lemma eq_sigT_fst X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2) :
x1 = x2.

Lemma eq_sigT_snd X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2) :
rew (eq_sigT_fst H) in H1 = H2.

Lemma eq_sig_fst X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2) :
x1 = x2.

Lemma eq_sig_snd X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2) :
rew (eq_sig_fst H) in H1 = H2.

Unset Implicit Arguments.

Exported hints

#[global]
Hint Resolve eq_dep_intro: core.
#[global]
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.
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.

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.
Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.

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.
Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_.

Uniqueness of Reflexive Identity Proofs is a direct instance of UIP
Streicher's axiom K is a direct consequence of Uniqueness of Reflexive Identity Proofs
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.
Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq.

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 := forall (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.
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.
Theorem UIP_shift : forall U, UIP_refl_ U -> forall x:U, UIP_refl_ (x = 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.
Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair.

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.

Lemma eq_rec_eq :
forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h.

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.

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.

Uniqueness of Reflexive Identity Proofs is a direct instance of UIP

Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x.

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.

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.

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).

Lemma eq_dep_non_dep :
forall U P p q x y, @eq_dep U (fun _ => P) p x q y -> x = y.

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.

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