From 1dee3f0f4384ba2afcf183a3821de4c10ae64557 Mon Sep 17 00:00:00 2001
From: kl-i <kl.i@icloud.com>
Date: Wed, 22 Sep 2021 11:24:08 +0100
Subject: [PATCH] Added feedbackG.md

---
 1FundamentalGroup/Quest2Part0.md | 79 ++++++++++++++++++++++++++++----
 1FundamentalGroup/feedbackG.md   | 44 ++++++++++++++++++
 2 files changed, 114 insertions(+), 9 deletions(-)
 create mode 100644 1FundamentalGroup/feedbackG.md

diff --git a/1FundamentalGroup/Quest2Part0.md b/1FundamentalGroup/Quest2Part0.md
index e7b19ec..2f03be6 100644
--- a/1FundamentalGroup/Quest2Part0.md
+++ b/1FundamentalGroup/Quest2Part0.md
@@ -8,12 +8,73 @@ 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 
-  an inverse map `predℤ : ℤ → ℤ`.
-- Turn `sucℤ` into a path `sucPath : ℤ ≡ ℤ` using `isoToPath`
-- 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`.
+1. Define a function `sucℤ : ℤ → ℤ` that increases every integer by one
+2. Prove that `sucℤ` is an isomorphism by constructing 
+   an inverse map `predℤ : ℤ → ℤ`.
+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`.
+5. 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`.
+
+In this part, we focus on `1` and `2`.
+
+## `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ℤ`.
diff --git a/1FundamentalGroup/feedbackG.md b/1FundamentalGroup/feedbackG.md
new file mode 100644
index 0000000..570fe02
--- /dev/null
+++ b/1FundamentalGroup/feedbackG.md
@@ -0,0 +1,44 @@
+# George feedback
+
+## Subject info
+
+- has some experience with type theory and haskell
+
+## Quest0/Part0
+
+- clarify the notation `a : A`
+- hide the imports
+- definition of inductive type doesn't make sense
+  without the further details.
+- confusion of `{!!}` and `{0}` and `?`
+- comparing holes to agda-info window is intuitive
+- error on firsts refine
+- add at each step what the agda-info window looks like
+- confusion about hole numbers. "just ignore them"
+- subject tries to read constraint in agda-info window. 
+  Shld deal with this somehow.
+- emphasize no need to fill holes in order.
+  
+## Quest0/Part1
+
+- subject confused about 'space of spaces'.
+  More specifically, need to say `a : A` means "`a` is a point of the space `A`".
+- we shld say `a ≡ b` means space of paths from `a` to `b`.
+- 'contradiction' is a pre-existing concept in subject brain.
+- "not sure that helps" - subject about definition of `Bool`
+- "is `flipPath` taking a point from `Bool` to another point of `Bool`
+  or is it taking a space to another space?"
+- "just some terminology" - subject on the definition of _fiber_.
+  Subject did not take in the picture of what it is called fiber.
+- need to add earlier how to check goal of holes.
+- need to be clear _we are assuming `flipPath` is constructed already_.
+- overall : need to be clearer that `Type` is space of spaces,
+  and paths in `Type` are saying which spaces are the same.
+
+## Quesst0/Part2
+
+- For the `iso` bit, change to just `C-c C-r` cuz `Iso` only has one constructor.
+- say you can check def of `Iso` by using `SPC c d`
+- say "just write `s` and `r` and write the rest then load".
+- emphasize agda is indentation sensitive.
+- subject unexpectedly extracts lemma `true ≡ true`.