Restate univalence

diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 6512d288ef7b32fc38dc59e91310ea34f5e2830b..1d4af7d2486829a3a3013a81b2af8f69feb751a2 100644 (file)
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -39,9 +39,9 @@ idToId (A B : U) (w : equiv A B)
       (transEquiv A B (transEquivToId A B w)) w
       (transIdFun A B w)
 
-univAx (A B : U) : isEquiv (Id U A B) (equiv A B) (transEquiv A B) =
-  gradLemma (Id U A B) (equiv A B) (transEquiv A B) (transEquivToId A B)
-            (idToId A B) (eqToEq A B)
+univalence (A B : U) : equiv (Id U A B) (equiv A B) =
+  (transEquiv A B,gradLemma (Id U A B) (equiv A B) (transEquiv A B)
+                            (transEquivToId A B) (idToId A B) (eqToEq A B))
 
 
 -- Alternative definition: