add standard formulation of univalence

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