From: coquand <coquand@chalmers.se>
Date: Mon, 27 Apr 2015 19:42:32 +0000 (+0200)
Subject: added some examples for pi1S2
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=83d2334f19379c90c797e84eda9a5af551db1686;p=cubicaltt.git

added some examples for pi1S2
---

diff --git a/examples/indSusp.ctt b/examples/indSusp.ctt
new file mode 100644
index 0000000..4d88d12
--- /dev/null
+++ b/examples/indSusp.ctt
@@ -0,0 +1,27 @@
+module indSusp where
+
+import susp
+
+suspOf (A X : U) : U = (u:X) * (v:X) * (A -> Id X u v)
+
+funToL (A X:U) (f:susp A -> X) : suspOf A X =
+  (f north,f south,\ (a:A) -> <i>f (merid{susp A} a@i))
+
+lToFun (A X:U) (z:suspOf A X) : susp A -> X = split
+ north -> z.1
+ south -> z.2.1
+ merid a @ i-> z.2.2 a @ i
+
+test1 (A X:U) (z:suspOf A X) : Id (suspOf A X) (funToL A X (lToFun A X z)) z
+   = refl (suspOf A X) z
+
+rem (A X:U) (f:susp A ->X) : (u:susp A) -> Id X (lToFun A X (funToL A X f) u) (f u) = split
+    north -> refl X (f north)
+    south -> refl X (f south)
+    merid a @ i -> refl X (f (merid{susp A} a @ i))
+
+test2 (A X:U) (f:susp A ->X) : Id (susp A ->X) (lToFun A X (funToL A X f)) f
+   = <i>\ (u:susp A) -> rem A X f u @ i
+
+funSusp (A X:U) : Id U (susp A -> X) (suspOf A X) =
+ isoId (susp A -> X) (suspOf A X) (funToL A X) (lToFun A X) (test1 A X) (test2 A X)
diff --git a/examples/mult.ctt b/examples/mult.ctt
new file mode 100644
index 0000000..4f3ccb9
--- /dev/null
+++ b/examples/mult.ctt
@@ -0,0 +1,59 @@
+module mult where
+
+import susp
+import helix
+
+-- another inverse function
+
+invS : S1 -> S1 = split
+ base -> base
+ loop @ i -> loop1 @ -i
+
+lemInv : (x:S1) -> Id S1 (mult x (invS x)) base = split 
+ base -> refl S1 base
+ loop @ i -> <j> loop1 @i\/-i\/j
+
+test0S : Z = winding (<i>mult (loop2@i) (invS (loop2@i)))
+test00S : Z = winding (<i>mult (loop4@i) (invS (loop4@i)))
+
+lemInv1 : (x:S1) -> Id S1 (mult (invS x) x) base = split
+ base -> refl S1 base
+ loop @ i -> <j> loop1 @ -i\/i\/j
+
+test : loopS1 = <i> mult (loop1@i) (loop1@-i)
+test1 : IdP (<i>Id S1 (mult (loop1@i) base) (mult (loop1@i) base)) loop1 loop1 = <i j> mult (loop1@i) (loop1@j)
+test2 : loopS1 = <i> mult (loop1@i) (loop1@i)
+test3 : Id loopS1 test2 (compS1 loop1 loop1) = refl loopS1 test2
+
+lemBase (y:S1) : Id S1 (mult base (mult base y)) y = 
+ compId S1 (mult base (mult base y)) (mult base y) y (idL (mult base y)) (idL y)
+
+{-
+corrInv (y:S1) : (x : S1) -> Id S1 (mult x (mult (invS x) y)) y = split
+ base -> lemBase y
+ loop @ i -> rem
+   where rem : Id S1 (mult (loop {S1} @ i) (mult (loop {S1} @ -i) y)) y =
+           transport (<j>Id S1 (mult (loop {S1} @ i/\j) (mult (loop {S1} @ -(i/\j)) y)) y) (lemBase y)
+-}
+
+corrInv (x y : S1) : Id S1 (mult x (mult (invS x) y)) y =
+ compId S1 (mult x (mult (invS x) y)) (mult (mult x (invS x)) y) y rem1 rem
+ where rem1 : Id S1 (mult x (mult (invS x) y)) (mult (mult x (invS x)) y) = multAssoc x (invS x) y
+
+       rem : Id S1 (mult (mult x (invS x)) y) y =
+        compId S1 (mult (mult x (invS x)) y) (mult base y) y  (<i>mult (lemInv x @i) y) (idL y)
+
+corrInv1 (x y : S1) : Id S1 (mult (invS x) (mult x y)) y =
+ compId S1 (mult (invS x) (mult x y)) (mult (mult (invS x) x) y) y rem1 rem
+ where rem1 : Id S1 (mult (invS x) (mult x y)) (mult (mult (invS x) x) y) = multAssoc (invS x) x y
+
+       rem : Id S1 (mult (mult (invS x) x) y) y =
+        compId S1 (mult (mult (invS x) x) y) (mult base y) y (<i>mult (lemInv1 x@i) y) (idL y)
+
+eqS1 (x:S1) : Id U S1 S1 = isoId S1 S1 (mult x) (mult (invS x)) (corrInv x) (corrInv1 x)
+
+-- we deduce the following fibration
+
+fibS1 (x:S1) : S1 -> U = split
+ base -> S1
+ loop @ i -> (eqS1 x) @ i
diff --git a/examples/truncS2.ctt b/examples/truncS2.ctt
new file mode 100644
index 0000000..980b970
--- /dev/null
+++ b/examples/truncS2.ctt
@@ -0,0 +1,36 @@
+module truncS2 where
+
+import ex1
+import indSusp
+
+-- is X is a set then Id U (aLoop X) X
+
+lemLoopSet (X:U) (sX: set X) : Id U (aLoop X) X
+ = isoId (aLoop X) X f g s t
+ where
+   f (z:  aLoop X) : X =  z.1
+   g (x: X) : aLoop X =  (x,refl X x)
+   s (y : X) : Id X (f (g y)) y =  refl X y
+   t (z : aLoop X) : Id (aLoop X) (g (f z)) z = <i>(z.1,sX z.1 z.1 (refl X z.1) z.2@i)
+
+lemS1Set (X : U) (sX: set X) : Id U (S1 -> X) X =
+ compId U (S1 -> X) (aLoop X) X (<i>thm X@-i) (lemLoopSet X sX)
+
+S2 : U = susp S1
+
+lemGrp1 (X : U) (gX: groupoid X) : Id U (suspOf S1 X) ((u:X) * (v : X) * Id X u v)
+   = <i> (u:X) * (v:X) * (lemS1Set (Id X u v) (gX u v) @ i)
+ 
+lemIdSig (X:U) :  Id U ((u:X) * (v:X) * Id X u v) X = isoId  ((u:X) * (v:X) * Id X u v) X f g s t
+ where
+  Z : U = (u:X) * (v:X) * Id X u v
+  f (z:Z) : X = z.1
+  g (x : X) : Z = (x,(x,refl X x))
+  s (y:X) : Id X (f (g y)) y = refl X y
+  t (z:Z) : Id Z (g (f z)) z = <i>(z.1,contrSingl X z.1 z.2.1 z.2.2 @ i)
+
+lemGrp2 (X : U) (gX:groupoid X) : Id U (suspOf S1 X) X = 
+ compId U (suspOf S1 X) ((u:X) * (v:X) * Id X u v) X (lemGrp1 X gX) (lemIdSig X)
+
+lemGrp3 (X : U) (gX: groupoid X) : Id U (S2 -> X) X =
+ compId U (S2 -> X) (suspOf S1 X) X (funSusp S1 X) (lemGrp2 X gX)