Identities over types satisfying Uniqueness of Identity Proofs

themselves satisfied Uniqueness of Identity Proofs. Otherwise said
uniqueness of equality proofs is enough to characterize types whose
equality has a degenerated "homotopical" structure (this is a short
proof of a result inspired by Voevodsky's proof of inclusion of
h-level n into h-level n+1).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16017 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 31 insertions, 0 deletions

diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index a22f286ed..0e9f39f6b 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -325,6 +325,29 @@ Section Equivalences.
 
 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 : forall U, UIP_refl_ U -> forall x:U, UIP_refl_ (x = x).
+Proof.
+  intros X UIP_refl x y.
+  rewrite (UIP_refl x y).
+  intros z.
+  assert (UIP:forall y' y'' : x = x, y' = y'').
+  { intros. apply eq_trans with (eq_refl x). apply UIP_refl. 
+    symmetry. apply UIP_refl. }
+  transitivity (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z)
+                         (eq_sym (UIP (eq_refl x) (eq_refl x)))).
+  - destruct z. unfold e. destruct (UIP _ _). reflexivity.
+  - change
+      (match eq_refl x as y' in _ = x' return y' = y' -> Type 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))))).
+    destruct z. unfold e. destruct (UIP _ _). reflexivity.
+Qed.
+
 Section Corollaries.
 
   Variable U:Type.
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 16c50b410..ea5b16517 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -326,6 +326,14 @@ Qed.
   (** Examples of short direct proofs of unicity of reflexivity proofs
       on specific domains *)
 
+Lemma UIP_refl_unit (x : tt = tt) : x = eq_refl tt.
+Proof.
+  change (match tt as b return tt = b -> Type with
+          | tt => fun x => x = eq_refl tt
+          end x).
+  destruct x; reflexivity.
+Defined.
+
 Lemma UIP_refl_bool (b:bool) (x : b = b) : x = eq_refl.
 Proof.
   destruct b.