-
Notifications
You must be signed in to change notification settings - Fork 134
/
Problem.agda
150 lines (103 loc) · 4.83 KB
/
Problem.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
-- An example of something where normalization is surprisingly slow
{-# OPTIONS --safe #-}
module Cubical.Experiments.Problem where
open import Cubical.Foundations.Prelude
open import Cubical.Data.Int
open import Cubical.HITs.S1
open import Cubical.HITs.S2
open import Cubical.HITs.S3
open import Cubical.HITs.Join
open import Cubical.Homotopy.Hopf
open S¹Hopf
ptType : Type _
ptType = Σ Type₀ \ A → A
pt : (A : ptType) → A .fst
pt A = A .snd
S¹pt : ptType
S¹pt = (S¹ , base)
S²pt : ptType
S²pt = (S² , base)
S³pt : ptType
S³pt = (S³ , base)
joinpt : ptType
joinpt = (join S¹ S¹ , inl base)
Ω : (A : ptType) → ptType
Ω A = Path _ (pt A) (pt A) , refl
Ω² : (A : ptType) → ptType
Ω² A = Ω (Ω A)
Ω³ : (A : ptType) → ptType
Ω³ A = Ω² (Ω A)
α : join S¹ S¹ → S²
α (inl _) = base
α (inr _) = base
α (push x y i) = (merid y ∙ merid x) i
where
merid : S¹ → Path S² base base
merid base = refl
merid (loop i) = λ j → surf i j
-- The tests
test0To2 : Ω³ S³pt .fst
test0To2 i j k = surf i j k
f3 : Ω³ S³pt .fst → Ω³ joinpt .fst
f3 p i j k = S³→joinS¹S¹ (p i j k)
test0To3 : Ω³ joinpt .fst
test0To3 = f3 test0To2
f4 : Ω³ joinpt .fst → Ω³ S²pt .fst
f4 p i j k = α (p i j k)
test0To4 : Ω³ S²pt .fst
test0To4 = f4 test0To3
innerpath : ∀ i j → HopfS² (test0To4 i j i1)
innerpath i j = transp (λ k → HopfS² (test0To4 i j k)) i0 base
-- C-c C-n problem uses a lot of memory
problem : pos 0 ≡ pos 0
problem i = transp (λ j → helix (innerpath i j)) i0 (pos 0)
-- Lots of tests: (thanks Evan!)
winding2 : Path (Path S² base base) refl refl → ℤ
winding2 p = winding (λ j → transp (λ i → HopfS² (p i j)) i0 base)
test0 : ℤ
test0 = winding2 (λ i j → surf i j)
test1 : ℤ
test1 = winding2 (λ i j → surf j i)
test2 : ℤ
test2 = winding2 (λ i j → hcomp (λ _ → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) (surf i j))
test3 : ℤ
test3 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) base)
test4 : ℤ
test4 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) base)
test5 : ℤ
test5 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → surf k i ; (j = i1) → base}) base)
test6 : ℤ
test6 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → surf k i}) base)
test7 : ℤ
test7 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → surf j k ; (j = i0) → base ; (j = i1) → base}) (surf i j))
test8 : ℤ
test8 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → surf k i ; (j = i1) → base}) (surf i j))
test9 : ℤ
test9 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → surf k i}) (surf i j))
test10 : ℤ
test10 = winding2 (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) (surf i j))
-- Tests using HopfS²'
winding2' : Path (Path S² base base) refl refl → ℤ
winding2' p = winding (λ j → transp (λ i → HopfS²' (p i j)) i0 base)
test0' : ℤ
test0' = winding2' (λ i j → surf i j)
test1' : ℤ
test1' = winding2' (λ i j → surf j i)
test2' : ℤ
test2' = winding2' (λ i j → hcomp (λ _ → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) (surf i j))
test3' : ℤ
test3' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) base)
test4' : ℤ
test4' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) base)
test5' : ℤ
test5' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → surf k i ; (j = i1) → base}) base)
test6' : ℤ
test6' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → surf k i}) base)
test7' : ℤ
test7' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → surf j k ; (j = i0) → base ; (j = i1) → base}) (surf i j))
test8' : ℤ
test8' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → surf k i ; (j = i1) → base}) (surf i j))
test9' : ℤ
test9' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → base ; (i = i1) → base ; (j = i0) → base ; (j = i1) → surf k i}) (surf i j))
test10' : ℤ
test10' = winding2' (λ i j → hcomp (λ k → λ { (i = i0) → surf j k ; (i = i1) → base ; (j = i0) → base ; (j = i1) → base}) (surf i j))