From: Anders <mortberg@chalmers.se>
Date: Thu, 18 Jun 2015 16:57:12 +0000 (+0200)
Subject: Restate univalence
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=67638e218f1c7f4c69d3df17628a246aa1e01e49;p=cubicaltt.git

Restate univalence
---

diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 6512d28..1d4af7d 100644
--- 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: