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
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 expressed as a non
dependent inductive type
Dependent equality is equivalent to equality on dependent pairs
Exported hints
Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
Invariance by Substitution of Reflexive Equality Proofs
Definition Eq_rect_eq :=
forall (
p:U) (
Q:U ->
Type) (
x:Q
p) (
h:p =
p),
x =
eq_rect p Q x p h.
Injectivity of Dependent Equality
Definition 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)
Definition UIP_ :=
forall (
x y:U) (
p1 p2:x =
y),
p1 =
p2.
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 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 of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq
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
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