diff options
| author | herbelin | 2012-12-04 23:26:10 +0000 |
|---|---|---|
| committer | herbelin | 2012-12-04 23:26:10 +0000 |
| commit | 34f8e2d160148e78abce969533739af8810d4347 (patch) | |
| tree | 43a80f6f08ab4d64a1ea6996d0355a15f6eb2b05 /plugins/xml/doubleTypeInference.ml | |
| 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 'plugins/xml/doubleTypeInference.ml')
0 files changed, 0 insertions, 0 deletions