projects
/
cubicaltt.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
1734296
)
add standard formulation of univalence
author
Anders Mörtberg
<andersmortberg@gmail.com>
Wed, 30 Dec 2015 18:58:37 +0000
(19:58 +0100)
committer
Anders Mörtberg
<andersmortberg@gmail.com>
Wed, 30 Dec 2015 18:58:37 +0000
(19:58 +0100)
examples/testContr.ctt
patch
|
blob
|
blame
|
history
diff --git
a/examples/testContr.ctt
b/examples/testContr.ctt
index 61d031b30fce94a7ac42d4f71e6e4e4d5a1302b4..95b50227e348377b68d7a5062993fbdc97b131ff 100644
(file)
--- a/
examples/testContr.ctt
+++ b/
examples/testContr.ctt
@@
-143,6
+143,8
@@
univalence (A X:U) : isEquiv (Id U X A) (equiv X A) (lem2 A X) = thmUniv lem2 A
corrUniv (A X:U) : Id U (Id U X A) (equiv X A) =
equivId (Id U X A) (equiv X A) (lem2 A X) (univalence A X)
+corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) = (lem2 B A,univalence B A)
+
testUniv1 (A:U) : Id U A A = trans (equiv A A) (Id U A A) (<i>corrUniv A A@-i) (idEquiv A)
-- obtained by normal form