Kubus

loopspacelib/loopspace.ktt

The loop space of the circle is the integers.

15 declarations, all certified by the kernel · source

1import circle
2
3✓def intLoopPos : Nat -> Path S1 base base
4 | zero => \i -> base
6
7✓def intLoopNeg : Nat -> Path S1 base base
11✓def intLoop : Int -> Path S1 base base
12 | pos n => intLoopPos n
15✓def decodeSquare : (n : Int) -> PathP (\i -> Path S1 base (loop i)) (intLoop (predInt n)) (intLoop n)
16 | pos zero => \i j -> loop (i \/ ~j)
17 | pos (suc n) => \i j -> fill k S1 [j = 0 -> base, j = 1 -> loop k] (intLoopPos n j) i
18 | negsuc n => \i j -> fill k S1 [j = 0 -> base, j = 1 -> loop (~k)] (intLoopNeg n j) (~i)
20✓def decode : (x : S1) -> helix x -> Path S1 base x
22 | loop i => \y j -> hcomp k S1 [i = 0 -> intLoop (predSuc y k) j, i = 1 -> intLoop y j,
23 j = 0 -> base, j = 1 -> loop i]
24 (decodeSquare (unglue y) i j)
26✓def encode (x : S1) (p : Path S1 base x) : helix x := transport (\i -> helix (p i)) (pos zero)
28✓def decodeEncode (x : S1) (p : Path S1 base x) : Path (Path S1 base x) (decode x (encode x p)) p :=
29 J (\x p -> Path (Path S1 base x) (decode x (encode x p)) p) (cong (decode base) (transportRefl (pos zero))) p
31-- Transport along helix, propositionally (composition does not compute away in Int in CCHM)
33-- transport along a composite path is the composite of the transports
34✓def substComp {X : U} (F : X -> U) {a b : X} (p : Path X a b) (u : F a) {c : X} (q : Path X b c)
35 : Path (F c) (transport (\i -> F (trans p q i)) u) (transport (\i -> F (q i)) (transport (\i -> F (p i)) u)) :=
36 J (\c q -> Path (F c) (transport (\i -> F (trans p q i)) u) (transport (\i -> F (q i)) (transport (\i -> F (p i)) u)))
37 (trans (cong (\(r : Path X a b) -> transport (\i -> F (r i)) u) (sym (rUnit p)))
38 (sym (transportRefl (transport (\i -> F (p i)) u))))
39 q
41-- transporting back undoes transport
42✓def transportInv {A B : U} (p : Path U A B) (x : A) : Path A (transport (\i -> p (~i)) (transport p x)) x :=
43 J^1 (\B p -> Path A (transport (\i -> p (~i)) (transport p x)) x)
44 (trans (cong (transport (\i -> A)) (transportRefl x)) (transportRefl x)) p
46✓def transportLoop (x : Int) : Path Int (sucInt x) (transport (\i -> helix (loopP i)) x) :=
49✓def transportInvLoop (y : Int) : Path Int (transport (\i -> helix (invLoop i)) y) (predInt y) :=
51 (transportInv (\i -> helix (loopP i)) (predInt y))
53✓def windingPos : (n : Nat) -> Path Int (winding (intLoopPos n)) (pos n)
58✓def windingNeg : (n : Nat) -> Path Int (winding (intLoopNeg n)) (negsuc n)
63✓def encodeDecode : (n : Int) -> Path Int (encode base (decode base n)) n
64 | pos n => windingPos n
67-- The loop space of the circle is the integers
68✓def loopSpaceS1 : Path U (Path S1 base base) Int :=