From: Simon Huber Date: Thu, 30 Apr 2015 13:32:40 +0000 (+0200) Subject: non-trivial homotopy in the loop space of stwo X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=88932806f440678a171b8a94a996255af4346852;p=cubicaltt.git non-trivial homotopy in the loop space of stwo --- diff --git a/examples/pi1S2output.ctt b/examples/pi1S2output.ctt new file mode 100644 index 0000000..a268409 --- /dev/null +++ b/examples/pi1S2output.ctt @@ -0,0 +1,17 @@ +module pi1S2output where + +import pi1S2 + +loopSpace : U = Id stwo north north + +aLoop1 : loopSpace = refl stwo north +aLoop2 : loopSpace = compId stwo north south north meridNstwo (meridSstwo@-i) + + + +test2Normal : Id pi1stwo trivstwo loopstwo = + inc ( comp stwo (comp stwo (comp stwo north [ (i2 = 1) -> comp stwo north [ (i1 = 1) -> comp stwo north [ (i4 = 1) -> comp stwo north [ (i5 = 1) -> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> merid {stwo} north @ -i4 ]) [ (i6 = 0) -> comp stwo north [ (i7 = 0) -> comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> comp stwo south [ (i8 = 0) -> comp stwo north [ (i10 = 0) -> comp stwo south [ (i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ], (i9 = 0) -> comp stwo south [ (i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ] ] ]) [ (i8 = 0) -> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> comp stwo north [ (i9 = 0) -> comp stwo south [ (i10 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ], (i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ] ]) [ (i9 = 0) -> comp stwo (comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> comp stwo south [ (i10 = 0) -> comp stwo north [ (i11 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ], (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ]) [ (i10 = 0) -> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> comp stwo north [ (i11 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ], (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ]) [ (i3 = 1) -> comp stwo north [ (i11 = 0)(i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ]) [ (i10 = 0) -> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> comp stwo north [ (i4 = 0) -> comp stwo north [ (i5 = 1) -> merid {stwo} north @ i6 ] ] ]) [ (i11 = 0) -> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ], (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ]) [ (i3 = 1) -> comp stwo north [ (i12 = 0)(i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ] ]) [ (i10 = 0) -> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> comp stwo north [ (i11 = 0) -> comp stwo north [ (i12 = 1)(i13 = 1) -> merid {stwo} north @ i14 ] ] ]) [ (i11 = 0) -> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> comp stwo north [ (i12 = 1) -> merid {stwo} north @ (i13 /\ i14) ] ]) [ (i12 = 1) -> comp stwo (merid {stwo} north @ (i13 /\ i3)) [ (i3 = 1) -> merid {stwo} north @ (i13 \/ i14) ] ]) [ (i3 = 1) -> comp stwo north [ (i12 = 1) -> merid {stwo} north @ i14, (i13 = 1) -> merid {stwo} north @ i14 ] ] ]) [ (i3 = 1) -> comp stwo north [ (i11 = 0)(i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ]) [ (i3 = 1) -> comp stwo south [ (i10 = 0)(i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ] ]) [ (i3 = 1) -> comp stwo north [ (i10 = 0)(i9 = 0) -> comp stwo south [ (i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ] ] ]) [ (i3 = 1) -> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> comp stwo south [ (i8 = 0) -> comp stwo north [ (i10 = 0) -> comp stwo south [ (i12 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ], (i11 = 0) -> comp stwo south [ (i12 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ] ] ]) [ (i8 = 0) -> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> comp stwo north [ (i10 = 0) -> comp stwo south [ (i11 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ], (i12 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ] ]) [ (i10 = 0) -> comp stwo (comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> comp stwo south [ (i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ], (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ]) [ (i11 = 0) -> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ], (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ]) [ (i9 = 0) -> comp stwo north [ (i12 = 0)(i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ]) [ (i11 = 0) -> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> comp stwo north [ (i10 = 0) -> comp stwo north [ (i11 = 1) -> merid {stwo} north @ i12 ] ] ]) [ (i12 = 0) -> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i15 = 1) -> merid {stwo} north @ i16 ], (i14 = 0) -> comp stwo north [ (i15 = 1) -> merid {stwo} north @ i16 ] ] ]) [ (i9 = 0) -> comp stwo north [ (i13 = 0)(i14 = 0) -> comp stwo north [ (i15 = 1) -> merid {stwo} north @ i16 ] ] ] ] ]) [ (i11 = 0) -> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1)(i14 = 1) -> merid {stwo} north @ i15 ] ] ]) [ (i12 = 0) -> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ (i14 /\ i15) ] ]) [ (i13 = 1) -> comp stwo (merid {stwo} north @ (i14 /\ -i9)) [ (i9 = 0) -> merid {stwo} north @ (i14 \/ i15) ] ]) [ (i9 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i15, (i14 = 1) -> merid {stwo} north @ i15 ] ] ]) [ (i9 = 0) -> comp stwo north [ (i12 = 0)(i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ]) [ (i9 = 0) -> comp stwo south [ (i11 = 0)(i12 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ] ]) [ (i9 = 0) -> comp stwo north [ (i10 = 0)(i11 = 0) -> comp stwo south [ (i12 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ] ] ] ]) [ (i8 = 1) -> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i9 = 0) -> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> merid {stwo} north @ (-i10 \/ -i11) ], (i9 = 1) -> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> merid {stwo} north @ (-i10 \/ -i11) ] ]) [ (i3 = 1) -> comp stwo (merid {stwo} north @ -i10) [ (i9 = 0) -> merid {stwo} north @ (-i10 /\ -i11), (i9 = 1) -> merid {stwo} north @ (-i10 /\ -i11) ] ] ] ] ] ] ] ] ]) [ (i1 = 1) -> comp stwo (comp stwo north [ (i2 = 1) -> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> merid {stwo} north @ -i4 ] ]) [ (i3 = 1) -> comp stwo (comp stwo north [ (i2 = 1) -> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> merid {stwo} north @ -i4 ] ]) [ (i4 = 0) -> comp stwo (comp stwo north [ (i2 = 1) -> comp stwo (merid {stwo} north @ (i5 /\ i6)) [ (i5 = 1)(i6 = 1) -> merid {stwo} north @ -i7 ] ]) [ (i2 = 1) -> comp stwo (merid {stwo} north @ (i5 \/ i6)) [ (i5 = 1) -> merid {stwo} north @ -i7, (i6 = 1) -> merid {stwo} north @ -i7 ] ], (i4 = 1) -> comp stwo (comp stwo (merid {stwo} north @ (i5 /\ i2)) [ (i2 = 1)(i5 = 1) -> merid {stwo} north @ -i6 ]) [ (i2 = 1) -> comp stwo (merid {stwo} north @ (i5 \/ i6)) [ (i5 = 1) -> merid {stwo} north @ -i7, (i6 = 1) -> merid {stwo} north @ -i7 ] ] ] ] ]) [ (i1 = 1) -> comp stwo (merid {stwo} north @ i2) [ (i2 = 1) -> merid {stwo} (comp sone north [ (i0 = 1) -> merid {sone} true @ i1 ]) @ -i3 ] ]) + + +test2loop : Id loopSpace aLoop1 aLoop2 = + comp stwo (comp stwo (comp stwo north [ (i2 = 1) -> comp stwo north [ (i1 = 1) -> comp stwo north [ (i4 = 1) -> comp stwo north [ (i5 = 1) -> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> merid {stwo} north @ -i4 ]) [ (i6 = 0) -> comp stwo north [ (i7 = 0) -> comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> comp stwo south [ (i8 = 0) -> comp stwo north [ (i10 = 0) -> comp stwo south [ (i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ], (i9 = 0) -> comp stwo south [ (i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ] ] ]) [ (i8 = 0) -> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> comp stwo north [ (i9 = 0) -> comp stwo south [ (i10 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ], (i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ] ]) [ (i9 = 0) -> comp stwo (comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> comp stwo south [ (i10 = 0) -> comp stwo north [ (i11 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ], (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ]) [ (i10 = 0) -> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> comp stwo north [ (i11 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ], (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ]) [ (i3 = 1) -> comp stwo north [ (i11 = 0)(i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ]) [ (i10 = 0) -> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> comp stwo north [ (i4 = 0) -> comp stwo north [ (i5 = 1) -> merid {stwo} north @ i6 ] ] ]) [ (i11 = 0) -> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ], (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ]) [ (i3 = 1) -> comp stwo north [ (i12 = 0)(i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ] ]) [ (i10 = 0) -> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> comp stwo north [ (i11 = 0) -> comp stwo north [ (i12 = 1)(i13 = 1) -> merid {stwo} north @ i14 ] ] ]) [ (i11 = 0) -> comp stwo (comp stwo (comp stwo north [ (i3 = 1) -> comp stwo north [ (i12 = 1) -> merid {stwo} north @ (i13 /\ i14) ] ]) [ (i12 = 1) -> comp stwo (merid {stwo} north @ (i13 /\ i3)) [ (i3 = 1) -> merid {stwo} north @ (i13 \/ i14) ] ]) [ (i3 = 1) -> comp stwo north [ (i12 = 1) -> merid {stwo} north @ i14, (i13 = 1) -> merid {stwo} north @ i14 ] ] ]) [ (i3 = 1) -> comp stwo north [ (i11 = 0)(i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ]) [ (i3 = 1) -> comp stwo south [ (i10 = 0)(i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ] ]) [ (i3 = 1) -> comp stwo north [ (i10 = 0)(i9 = 0) -> comp stwo south [ (i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i14 ] ] ] ] ] ]) [ (i3 = 1) -> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> comp stwo south [ (i8 = 0) -> comp stwo north [ (i10 = 0) -> comp stwo south [ (i12 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ], (i11 = 0) -> comp stwo south [ (i12 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ] ] ]) [ (i8 = 0) -> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> comp stwo north [ (i10 = 0) -> comp stwo south [ (i11 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ], (i12 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ] ]) [ (i10 = 0) -> comp stwo (comp stwo (comp stwo (comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> comp stwo south [ (i11 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ], (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ]) [ (i11 = 0) -> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ], (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ]) [ (i9 = 0) -> comp stwo north [ (i12 = 0)(i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ]) [ (i11 = 0) -> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> comp stwo north [ (i10 = 0) -> comp stwo north [ (i11 = 1) -> merid {stwo} north @ i12 ] ] ]) [ (i12 = 0) -> comp stwo (comp stwo (merid {stwo} north @ -i9) [ (i9 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i15 = 1) -> merid {stwo} north @ i16 ], (i14 = 0) -> comp stwo north [ (i15 = 1) -> merid {stwo} north @ i16 ] ] ]) [ (i9 = 0) -> comp stwo north [ (i13 = 0)(i14 = 0) -> comp stwo north [ (i15 = 1) -> merid {stwo} north @ i16 ] ] ] ] ]) [ (i11 = 0) -> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> comp stwo north [ (i12 = 0) -> comp stwo north [ (i13 = 1)(i14 = 1) -> merid {stwo} north @ i15 ] ] ]) [ (i12 = 0) -> comp stwo (comp stwo (comp stwo north [ (i9 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ (i14 /\ i15) ] ]) [ (i13 = 1) -> comp stwo (merid {stwo} north @ (i14 /\ -i9)) [ (i9 = 0) -> merid {stwo} north @ (i14 \/ i15) ] ]) [ (i9 = 0) -> comp stwo north [ (i13 = 1) -> merid {stwo} north @ i15, (i14 = 1) -> merid {stwo} north @ i15 ] ] ]) [ (i9 = 0) -> comp stwo north [ (i12 = 0)(i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ]) [ (i9 = 0) -> comp stwo south [ (i11 = 0)(i12 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ] ]) [ (i9 = 0) -> comp stwo north [ (i10 = 0)(i11 = 0) -> comp stwo south [ (i12 = 0) -> comp stwo north [ (i13 = 0) -> comp stwo north [ (i14 = 1) -> merid {stwo} north @ i15 ] ] ] ] ] ] ]) [ (i8 = 1) -> comp stwo (comp stwo (merid {stwo} north @ i3) [ (i9 = 0) -> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> merid {stwo} north @ (-i10 \/ -i11) ], (i9 = 1) -> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> merid {stwo} north @ (-i10 \/ -i11) ] ]) [ (i3 = 1) -> comp stwo (merid {stwo} north @ -i10) [ (i9 = 0) -> merid {stwo} north @ (-i10 /\ -i11), (i9 = 1) -> merid {stwo} north @ (-i10 /\ -i11) ] ] ] ] ] ] ] ] ]) [ (i1 = 1) -> comp stwo (comp stwo north [ (i2 = 1) -> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> merid {stwo} north @ -i4 ] ]) [ (i3 = 1) -> comp stwo (comp stwo north [ (i2 = 1) -> comp stwo (merid {stwo} north @ i3) [ (i3 = 1) -> merid {stwo} north @ -i4 ] ]) [ (i4 = 0) -> comp stwo (comp stwo north [ (i2 = 1) -> comp stwo (merid {stwo} north @ (i5 /\ i6)) [ (i5 = 1)(i6 = 1) -> merid {stwo} north @ -i7 ] ]) [ (i2 = 1) -> comp stwo (merid {stwo} north @ (i5 \/ i6)) [ (i5 = 1) -> merid {stwo} north @ -i7, (i6 = 1) -> merid {stwo} north @ -i7 ] ], (i4 = 1) -> comp stwo (comp stwo (merid {stwo} north @ (i5 /\ i2)) [ (i2 = 1)(i5 = 1) -> merid {stwo} north @ -i6 ]) [ (i2 = 1) -> comp stwo (merid {stwo} north @ (i5 \/ i6)) [ (i5 = 1) -> merid {stwo} north @ -i7, (i6 = 1) -> merid {stwo} north @ -i7 ] ] ] ] ]) [ (i1 = 1) -> comp stwo (merid {stwo} north @ i2) [ (i2 = 1) -> merid {stwo} (comp sone north [ (i0 = 1) -> merid {sone} true @ i1 ]) @ -i3 ] ]