added imports and changed collection.ctt (corrUniv B A)

diff --git a/examples/collection.ctt b/examples/collection.ctt
index ee294b960e9cd9aa61c26b0c7d0fa75fe45d4bb6..d68f71053d442a83a29073c19929df7e85947561 100644 (file)
--- a/examples/collection.ctt
+++ b/examples/collection.ctt
@@ -1,10 +1,13 @@
 module collection where
 
+import prelude
+import equiv
+import univalence
 import sigma
 import pi
-import testContr
+-- import testContr
 
-propIsContr (A:U) (z0 z1:isContr A) : Id (isContr A) z0 z1 =
+propIsContr (A:U) (z0 z1 : isContr A) : Id (isContr A) z0 z1 =
  <j>(p0 a1@j,
      \ (x:A) -> 
         <i>comp (<_>A) (lem1 x@i@j) [ (i=0) -> <k>p0 a1@j, (i=1) -> <k>p0 x@(j\/k),
@@ -33,7 +36,7 @@ lem5 (A B : U) (gB:groupoid B) (t u:equiv A B) : set (Id (equiv A B) t u)
  = substInv U set  (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (groupoidFun A B gB t.1 u.1)
 
 lem6 (A B : U) (sB : set B) : set (Id U A B) = 
- substInv U set (Id U A B)  (equiv A B) (corrUniv B A) (lem4 A B sB)
+ substInv U set (Id U A B)  (equiv A B) (corrUniv A B   ) (lem4 A B sB)
 
 -- the collection of all sets
 

diff --git a/examples/groupoidTrunc.ctt b/examples/groupoidTrunc.ctt
index a1664868eb0f56dfc9f6c9cb1033b7fcafd9ab70..1f4502d2897e4b490e833f93984c7b05e0edd7c4 100644 (file)
--- a/examples/groupoidTrunc.ctt
+++ b/examples/groupoidTrunc.ctt
@@ -1,6 +1,8 @@
 module groupoidTrunc where
 
 import prelude
+import equiv
+
 
 data gTrunc (A : U)
   = inc (a : A)

diff --git a/examples/hnat.ctt b/examples/hnat.ctt
index d4c8a8f0b39e4bab3b6da0122bf3bfbc353e2a64..005ed28fbb59d1272bff2a59e8e46586863272ee 100644 (file)
--- a/examples/hnat.ctt
+++ b/examples/hnat.ctt
@@ -1,6 +1,7 @@
 module hnat where
 
 import nat
+import equiv
 
 -- Non-standard nat:
 hdata hnat = nzero

diff --git a/examples/int.ctt b/examples/int.ctt
index 16e8e5e69bf0710e69db41e17aabc29b3ef4df90..5ff3ccda0d92b7232cb50ddcb207ae07fbf9fcbf 100644 (file)
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -1,5 +1,6 @@
 module int where\r
 \r
+import equiv\r
 import nat\r
 import discor\r
 \r
@@ -60,4 +61,4 @@ sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ
 testOneZ : Z = transport sucIdZ zeroZ\r
 testNOneZ : Z = transport (<i> sucIdZ @ - i) zeroZ\r
 \r
-ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)
\ No newline at end of file
+ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)\r

diff --git a/examples/interval.ctt b/examples/interval.ctt
index 89a85dae8ffd27fbf4d222fcb33ce16bcdeb3e18..9029372dd6d8f3a945a73961a222f2f05074d497 100644 (file)
--- a/examples/interval.ctt
+++ b/examples/interval.ctt
@@ -1,6 +1,8 @@
 module interval where
 
 import gradLemma
+import equiv
+
 
 data I = zero | one | seg <i> [(i = 0) -> zero, (i = 1) -> one]
 

diff --git a/examples/pi.ctt b/examples/pi.ctt
index 2f1369bcd3c6730acb5c42ccc43c1ebea7f4a3eb..1c957b160bd811c8aeeb57a001445486294ad4ce 100644 (file)
--- a/examples/pi.ctt
+++ b/examples/pi.ctt
@@ -1,6 +1,7 @@
 module pi where
 
 import prelude
+import equiv
 
               -----------------------------------
               -- Example: Equality in pi types --

diff --git a/examples/prop.ctt b/examples/prop.ctt
index f9af4ede5c90d0c7b61420c6de0b1ee13d6a6ca7..e00387dea4ff82b11372b6f1736e40155f1f673c 100644 (file)
--- a/examples/prop.ctt
+++ b/examples/prop.ctt
@@ -1,6 +1,7 @@
 module prop where
 
 import prelude
+import equiv
 
 lemProp (A B : U) (f : A -> B) (g : B -> A)
       (s : (y:B) -> Id B (f (g y)) y)

diff --git a/examples/sigma.ctt b/examples/sigma.ctt
index 1053e700ea313dc88215579e9d2ac6913fbf4620..f34e5aa4072d0969a5fc2b4e27b9ee62d9e77b42 100644 (file)
--- a/examples/sigma.ctt
+++ b/examples/sigma.ctt
@@ -1,6 +1,7 @@
 module sigma where
 
 import prelude
+import equiv
 
 -- application of this fact