From: coquand <coquand@chalmers.se>
Date: Tue, 29 Dec 2015 15:16:37 +0000 (+0100)
Subject: updated collection
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9da12cd5f777c8c12b2504fc4ad0d3d06efd9524;p=cubicaltt.git

updated collection
---

diff --git a/examples/collection.ctt b/examples/collection.ctt
index 984f6e2..ee294b9 100644
--- a/examples/collection.ctt
+++ b/examples/collection.ctt
@@ -2,8 +2,22 @@ module collection where
 
 import sigma
 import pi
-import univalence
-import retract
+import testContr
+
+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),
+                                      (j=0) -> <k>p0 x@(i/\k), (j=1) -> <k>p1 x@i ])
+ where
+  a0 : A = z0.1
+  p0 : (x:A) -> Id A a0 x = z0.2
+  a1 : A = z1.1
+  p1 : (x:A) -> Id A a1 x = z1.2
+  lem1 (x:A) : IdP (<i>Id A a0 (p1 x@i)) (p0 a1) (p0 x) = <i j> p0 (p1 x@i) @ j
+ 
+propIsEquiv (A B : U) (f : A -> B)
+  : prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> <i> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i
 
 setFun (A B:U) (sB: set B) : set (A -> B) = setPi A (\ (x:A) -> B) (\ (x:A) -> sB)
 
@@ -19,7 +33,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) (univalence1 A B) (lem4 A B sB)
+ substInv U set (Id U A B)  (equiv A B) (corrUniv B A) (lem4 A B sB)
 
 -- the collection of all sets
 
diff --git a/examples/sigma.ctt b/examples/sigma.ctt
index faee60c..cd124eb 100644
--- a/examples/sigma.ctt
+++ b/examples/sigma.ctt
@@ -33,10 +33,7 @@ funDepTr (A:U) (P:A->U) (a0 a1 :A) (p:Id A a0 a1) (u0:P a0) (u1:P a1) :
 
 lem2 (A:U) (B:A-> U) (t u : sig A B) (p:Id A t.1 u.1) : 
   Id U  (IdP (<i>B (p@i)) t.2 u.2) (Id (B u.1) (transport (<i>B (p@i)) t.2) u.2) =
-    funDepTr (B t.1) (B u.1) P t.2 u.2
- where P : Id U (B t.1) (B u.1) = <i>B (p@i)
-       T0 : U = IdP P t.2 u.2
-       T1 : U = Id (B u.1) (transport P t.2) u.2
+    funDepTr A B t.1 u.1 p  t.2 u.2
 
 corSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) (p:Id A t.1 u.1) : 
   prop (IdP (<i>B (p@i)) t.2 u.2) = substInv U prop T0 T1 rem rem1
@@ -93,7 +90,7 @@ lem3 (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) (p:Id A t.1 u.1)
  where P : Id U (B t.1) (B u.1) = <i>B (p@i)
        T0 : U = IdP P t.2 u.2
        T1 : U = Id (B u.1) (transport P t.2) u.2
-       rem : Id U T0 T1 = funDepTr (B t.1) (B u.1) P t.2 u.2 -- lem2 A B t u p -- 
+       rem : Id U T0 T1 = lem2 A B t u p 
        v2 : B u.1 = transport P t.2
        rem1 : prop T1 = propSet (B u.1) (pB u.1) v2 u.2
        rem2 : T0 = transport (<i>rem@-i) (pB u.1 v2 u.2)
diff --git a/examples/testContr.ctt b/examples/testContr.ctt
index 2d7b3a4..c65dafd 100644
--- a/examples/testContr.ctt
+++ b/examples/testContr.ctt
@@ -77,7 +77,6 @@ equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (sig A B)
                          (retFunFib A B C f x z)
                          (isEquivContr (sig A B) (sig A C) cB cC (totalFun A B C f) (x,z))
 
-
 lemSinglContr (A:U) (a:A) : isContr ((x:A) * Id A a x) =
  ((a,refl A a),\ (z:(x:A) * Id A a x) -> contrSingl A a z.1 z.2)