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
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
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
- 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
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
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.
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.
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 expressed as a non
dependent inductive type
Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop :=
eq_dep1_intro : forall h:q = p, x = eq_rect q P y p h -> 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.
Implicit Arguments eq_dep [U P].
Implicit Arguments eq_dep1 [U P].
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.
Notation eq_sigS_eq_dep := eq_sigT_eq_dep (only parsing).
Lemma equiv_eqex_eqdep :
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.
Exported hints
Invariance by Substitution of Reflexive Equality Proofs
Injectivity of Dependent Equality
Uniqueness of Identity Proofs (UIP)
Uniqueness of Reflexive Identity Proofs
Streicher's axiom K
Injectivity of Dependent Equality is a consequence of
Invariance by Substitution of Reflexive Equality Proof
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__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.
Uniqueness of Identity Proofs (UIP) is a consequence of
Injectivity of Dependent Equality
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
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 to prove 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.
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 to prove 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 implies the injectivity of equality on dependent pairs in Type
Definition Inj_dep_pair :=
forall (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y.
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.
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
Uniqueness of Identity Proofs (UIP) is a consequence of
Injectivity of Dependent Equality
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
Lemma Streicher_K :
forall (x:U) (P:x = x -> Prop), P (refl_equal 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.
Implicit Arguments eq_dep [].
Implicit Arguments eq_dep1 [].