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
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
Dependent equality
Equivalent definition of dependent equality as a dependent pair of
equalities
Dependent equality is equivalent to equality on dependent pairs
Dependent equality is equivalent to a dependent pair of equalities
Exported hints
Hint Resolve eq_dep_intro: core.
Hint Immediate eq_dep_sym: core.
Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
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
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 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).
UIP implies the injectivity of equality on dependent pairs in Type
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 (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
UIP implies the injectivity of equality on dependent pairs in Type
Basic facts about eq_dep