Quest2/Part0,Part1 finished

1FundamentalGroup/Quest2.agda

@@ -0,0 +1,47 @@
+module 1FundamentalGroup.Quest2 where
+
+open import Cubical.Core.Everything
+open import Cubical.Data.Nat
+open import Cubical.Data.Int using (ℤ ; pos ; negsuc ; -_)
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude renaming (subst to endPt)
+open import Cubical.HITs.S1 using (S¹ ; base ; loop)
+open import 1FundamentalGroup.Quest1
+
+sucℤ : ℤ → ℤ
+sucℤ (pos n) = pos (suc n)
+sucℤ (negsuc zero) = pos zero
+sucℤ (negsuc (suc n)) = negsuc n
+
+predℤ : ℤ → ℤ
+predℤ (pos zero) = negsuc zero
+predℤ (pos (suc n)) = pos n
+predℤ (negsuc n) = negsuc (suc n)
+
+sucℤIso : Iso ℤ ℤ
+sucℤIso = iso sucℤ predℤ s r where
+
+  s : section sucℤ predℤ
+  s (pos zero) = refl
+  s (pos (suc n)) = refl
+  s (negsuc zero) = refl
+  s (negsuc (suc n)) = refl
+
+  r : retract sucℤ predℤ
+  r (pos zero) = refl
+  r (pos (suc n)) = refl
+  r (negsuc zero) = refl
+  r (negsuc (suc n)) = refl
+
+sucℤPath : ℤ ≡ ℤ
+sucℤPath = isoToPath sucℤIso
+
+helix : S¹ → Type
+helix base = ℤ
+helix (loop i) = sucℤPath i
+
+spinCountBase : base ≡ base → ℤ
+spinCountBase p = endPt helix p 0
+
+spinCount : (x : S¹) → base ≡ x → helix x
+spinCount x p = endPt helix p 0

1FundamentalGroup/Quest2Part0.md

@@ -8,12 +8,80 @@ allowing us to distinguish between all loops on `S¹`.
 
 The plan is :
 
-- Define a function `sucℤ : ℤ → ℤ` that increases every integer by one
-- Prove that `sucℤ` is an isomorphism by constructing 
+1. Define a function `sucℤ : ℤ → ℤ` that increases every integer by one
+2. Prove that `sucℤ` is an isomorphism by constructing 
    an inverse map `predℤ : ℤ → ℤ`.
-- Turn `sucℤ` into a path `sucPath : ℤ ≡ ℤ` using `isoToPath`
-- Define `helix : S¹ → Type` by mapping `base` to `ℤ` and
+3. Turn `sucℤ` into a path `sucPath : ℤ ≡ ℤ` using `isoToPath`
+4. Define `helix : S¹ → Type` by mapping `base` to `ℤ` and
    a generic point `loop i` to `sucPath i`.
-- Use `helix` and `endPt` to define the map `base ≡ x → helix x`
-  on all `x : S¹`, in particular giving us `Ω S¹ base → ℤ`
-  when applied to `base`.
+5. Use `helix` and `endPt` to define the map 
+   `spinCountBase : base ≡ base → ℤ`
+   Intuitively it counts how many times a path loops around `S¹`. 
+   a generic point `loop i` to `sucPath i`.
+6. Generalize this across the circle.
+
+In this part, we focus on `1`, `2` and `3`.
+
+## `sucℤ`
+
+- Setup the definition of `sucℤ` so that it looks of the form : 
+  ```agda
+  Name : TypeOfSpace
+  Name inputs = ?
+  ```
+  
+  Compare it with our solutions in `1FundamentalGroup/Quest1.agda`
+- We will define `sucℤ` the same way we defined `loop_times` : 
+  by induction.
+  Do cases on the input of `sucℤ`.
+  You should have something like :
+  ```agda
+  sucℤ : ℤ → ℤ
+  sucℤ pos n = ?
+  sucℤ negsuc n = ?
+  ```
+- For the non-negative integers `pos n` we want to map to its successor.
+  Recall that the `n` here is a point of the naturals `ℕ` whose definition is :
+  ```agda
+  data ℕ : Type where
+    zero : ℕ
+    suc : ℕ → ℕ
+  ```
+  Use `suc` to map `pos n` to its successor.
+- The negative integers require a bit more care.
+  Recall that annoyingly `negsuc n` means "`- (n + 1)`".
+  We want to map `- (n + 1)` to `- n`.
+  Try doing this. 
+  Then realise "you run out of negative integers at `-(0 + 1)`"
+  so you must do cases on `n` and treat the `-(0 + 1)` case separately.
+  <p>
+  <details>
+  <summary>Hint</summary>
+  
+  Do `C-c C-c` on `n`.
+  Then map `negsuc 0` to `pos 0`. 
+  For `negsuc (suc n)`, map it to `negsuc n`.
+  
+  </details>
+  </p>
+- This completes the definition of `sucℤ`.
+  Use `C-c C-n` to check it computes correctly.
+  E.g. check that `sucℤ (- 1)` computes to `pos 0`
+  and `sucℤ (pos 0)` computes to `pos 1`.
+  
+## `sucℤ` is an isomorphism
+
+- The goal is to define `predℤ : ℤ → ℤ` which 
+  "takes `n` to its predecessor `n - 1`".
+  This will act as the (homotopical) inverse of `sucℤ`.
+  Now that you have experience from defining `sucℤ`,
+  try defining `predℤ`.
+- Imitating what we did with `flipIso` and 
+  give a point `sucℤIso : ℤ ≅ ℤ`
+  by using `predℤ` as the inverse and proving
+  `section sucℤ predℤ` and `retract sucℤ predℤ`. 
+
+## `sucℤ` is a path
+
+- Imitating what we did with `flipPath`, 
+  upgrade `sucℤIso` to `sucℤPath`.

1FundamentalGroup/Quest2Part1.md

@@ -0,0 +1,54 @@
+# Comparison maps between `Ω S¹ base` and `ℤ`
+
+## The `ℤ`-bundle `helix`
+
+We want to make a `ℤ`-bundle over `S¹` by 
+'copying ℤ across the loop via `sucℤPath`'.
+In `Quest2.agda` locate
+
+```agda
+helix : S¹ → Type
+helix = {!!}
+```
+
+Try to imitate the definition of `doubleCover` to define the bunlde `helix`.
+You should compare your definition to ours in `Quest2Solutions.agda`.
+Note that we have called this `helix`, since the picture of this `ℤ`-bundle 
+looks like
+
+<img src="images/helix.png"
+     alt="helix"
+     width="1000"
+     class="center"/>
+
+## Counting loops
+
+Now we can do what was originally difficult - constructing an inverse map 
+(over all points). 
+Now we want to be able to count how many times a path `base ≡ base` loops around
+`S¹`, which we can do now using `helix` and finding end points of 'lifted' paths.
+For example the path `loop` should loop around once, 
+counted by looking at the end point of 'lifted' `loop`, starting at `0`.
+Hence try to define
+
+```agda
+spinCountBase : base ≡ base → helix base
+spinCountBase = {!!}
+```
+
+Try computing a few values using `C-c C-n`,
+you can try it on `refl`, `loop`, `loop 3 times`, `loop (- 1) times` and so on.
+
+## Generalising
+
+The function `spinCountBase`
+can actually be improved without any extra work to a function on all of `S¹`
+
+```agda
+spinCount : (x : S¹) → base ≡ x → helix x
+spinCount = {!!}
+```
+
+We will show that this and a general version of `loop_times` are
+inverses of each other over `S¹`, in particular obtaining an isomorphism
+between `base ≡ base` and `ℤ`.