From: Georgy Dunaev <georgedunaev@gmail.com>
Date: Sun, 6 Mar 2016 09:06:12 +0000 (+0300)
Subject: added imports and changed collection.ctt (corrUniv B A)
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=6bbb70cdb272410de1ee3a85000aae262c4a9959;p=cubicaltt.git

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

diff --git a/examples/collection.ctt b/examples/collection.ctt
index ee294b9..d68f710 100644
--- 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 a166486..1f4502d 100644
--- 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 d4c8a8f..005ed28 100644
--- 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 16e8e5e..5ff3ccd 100644
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -1,5 +1,6 @@
 module int where
 
+import equiv
 import nat
 import discor
 
@@ -60,4 +61,4 @@ sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ
 testOneZ : Z = transport sucIdZ zeroZ
 testNOneZ : Z = transport (<i> sucIdZ @ - i) zeroZ
 
-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)
diff --git a/examples/interval.ctt b/examples/interval.ctt
index 89a85da..9029372 100644
--- 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 2f1369b..1c957b1 100644
--- 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 f9af4ed..e00387d 100644
--- 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 1053e70..f34e5aa 100644
--- a/examples/sigma.ctt
+++ b/examples/sigma.ctt
@@ -1,6 +1,7 @@
 module sigma where
 
 import prelude
+import equiv
 
 -- application of this fact