diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-04 23:26:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-04 23:26:10 +0000 |
| commit | 34f8e2d160148e78abce969533739af8810d4347 (patch) | |
| tree | 43a80f6f08ab4d64a1ea6996d0355a15f6eb2b05 /theories/Logic/Eqdep_dec.v | |
| parent | 68edc2c4b99c18900f623bc3f08d49b17a27129b (diff) | |
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
Diffstat (limited to 'theories/Logic/Eqdep_dec.v')
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 8 |
1 files changed, 8 insertions, 0 deletions
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. |