Cleanup of 1FundamentalGroup/Quest0Part0

1FundamentalGroup/Quest0.agda

@@ -29,6 +29,9 @@ Flip : Bool → Bool
 Flip false = true
 Flip true = false
 
+-- notice we used `refl` instead of `λ i → false`,
+-- you might want to find out what `refl` does
+-- by looking up the definition
 flipIso : Bool ≅ Bool
 flipIso = iso Flip Flip s r where
   s : section Flip Flip
@@ -85,7 +88,7 @@ endPtOfTrue p = endPt doubleCover p true
 
 {-
 
-You can check that `SubstTrue refl` and `SubstTrue loop`
+You can check that `SubstTrue Refl` and `SubstTrue loop`
 are using `C-c C-n`
 
 -}
@@ -102,10 +105,10 @@ gives us a path in `B` from `f x` to `f y`
 We can use the above to get the contradiction we want
 by
 
-- assuming `p : refl ≡ loop`
+- assuming `p : Refl ≡ loop`
-- deducing `SubstTrue refl ≡ SubstTrue loop` using `cong`
+- deducing `SubstTrue Refl ≡ SubstTrue loop` using `cong`
 
 -}
 
-refl≢loop : refl ≡ loop → ⊥
+Refl≢loop : Refl ≡ loop → ⊥
-refl≢loop p = true≢false (cong endPtOfTrue p)
+Refl≢loop p = true≢false (cong endPtOfTrue p)

1FundamentalGroup/Quest0Part0.md

@@ -9,8 +9,8 @@ We begin by formalising the problem statement.
 
 A contruction of 'the circle' is :
 
-- a point
+- a point called `base`
-- an edge from that point to itself
+- an edge from that point to itself called `loop`
 
 Here is our definition of the circle in `agda`.
 
@@ -23,6 +23,27 @@ data S¹ : Type where
 The `base ≡ base` is the _space of paths from `base` to `base`_.
 The definition asserts that there is a point called `loop`
 in `base ≡ base`, i.e. a path from `base` to itself.
+Whenever we have a colon like `S¹ : Type` or `base : S¹`
+it says the former is a point in the latter, 
+where the latter is viewed as a space;
+in the first case `Type` is the space of spaces.
+
+<p>
+<details>
+<summary>Further details</summary>
+
+This is called a __higher inductive type_ (HIT), which generally
+follows the format of
+
+- `data` 
+- the name of the HIT - in our case `S¹`
+- the _type_ of the HIT, in our case `Type`
+- `where` followed by
+- the _constructors_ of the HIT, in our case `base` and `loop`,
+  which we will think of as vertices, edges, surfaces, and so on
+  
+</details>
+</p>
 
 An "edge" is the same as a path.
 There are other paths in `S¹`, 
@@ -83,6 +104,8 @@ We will fill the hole `{ }0`.
 - the number of holes in the `*Agda Information*` 
   window should have gone down by one,
   this means `agda` has accepted what you filled this hole with.
+  Just to be sure you can also reload the `agda` file and check
+  that `agda` has no complaints.
 - if you want to play around with this you can start again 
   by replacing what you wrote with `?` and doing
   `C-c C-l` 

1FundamentalGroup/Quest0Part1.md

@@ -1,13 +1,7 @@
-# `refl ≡ loop` is empty
+# `Refl ≡ loop` is empty
-
-To get a better feel of `S¹`, we show that the space
-
-```
-refl ≡ loop
-```
-
-is empty. 
 
+To get a better feel of `S¹`, we show that the space of paths (homotopies) between
+`Refl` and `loop`, written `Refl ≡ loop`, is empty. 
 First, we define the empty space and what it means for a space to be empty.
 Here is what this looks like in `agda` :
 
@@ -15,20 +9,20 @@ Here is what this looks like in `agda` :
 data ⊥ : Type where 
 ```
 
-This says "the empty space is a space with no points in it".
+This says "the empty space `⊥` is a space with no points in it".
 
-Here are two candidate definitions for a space `A` to be empty :
+Here are three candidate definitions for a space `A` to be empty :
 
-- there is a point `f : A → ⊥`
+- there is a point `f : A → ⊥` in the space of functions from `A` to the empty space
-- there is a path `p : A ≡ ⊥` in the space of spaces `Type`
+- there is a path `p : A ≡ ⊥` in the space of spaces `Type` from `A` to the empty space
 - there is an isomorphism `i : A ≅ ⊥` of spaces
 
-These turn out to be 'the same',
+These turn out to be 'the same' (see `1FundamentalGroup/Quest0SideQuests/SideQuest0`),
 however for our present purposes we will use the first definition.
-So our goal now is to produce a point of 
+Our goal is therefore to produce a point in the function space 
 
 ```agda
-( refl ≡ loop ) → ⊥
+( Refl ≡ loop ) → ⊥
 ```
 
 The authors of this series have thought long and hard
@@ -36,12 +30,14 @@ about how one would come up with the following argument.
 Unfortunately, sometimes mathematics is in need of a new trick
 and this was one of them.
 
-> The trick is to create a map from `refl ≡ loop` to `true ≡ false` by
+> The trick is to make a path `p : true ≡ false` from the assumed path (homotopy) `h : Refl ≡ loop` by
 > constructing a non-trivial `Bool`-bundle over the circle, 
-> hence obtaining a map `( refl ≡ loop ) → ⊥`.
+> hence obtaining a map `( Refl ≡ loop ) → ⊥`.
 
 To elaborate : 
 `Bool` here refers to the discrete space with two points `true, false`.
+(To find out the definition of `Bool` in `agda` 
+you can hover over `Bool` in `agda` and use `M-SPC c d`.)
 We will create a map `doubleCover : S¹ → Type` that sends
 `base` to `Bool` and the path `loop` to a non-trivial path `flipPath : Bool ≡ Bool`
 in the space of spaces.
@@ -51,6 +47,13 @@ for each point `x : S¹`,
 we call `doubleCover x` the _fiber of `doubleCover` over `x`_.
 All the fibers look like `Bool`, hence our choice of the name _`Bool`-bundle_.
 
+We will get a path from `true` to `false` 
+in the fiber of `doubleCover` over `base`
+by 'lifting the homotopy' `h : Refl ≡ loop` and considering the end points of 
+the 'lifted paths'.
+`Refl` will 'lift' to a 'constant path' and `loop` will 'lift' to 
+(Insert picture of 'lift' of `loop`)
+
 Let's assume for the moment that we have `flipPath` already and
 define `doubleCover`.
 
@@ -62,6 +65,7 @@ define `doubleCover`.
   ```
 - Navigate your cursor to the hole,
   write `x` and do `C-c C-c`.
+  The `c` stands for _cases_.
   You should now see two new holes : 
   
   ```agda
@@ -70,9 +74,9 @@ define `doubleCover`.
   doubleCover (loop i) = {!!} 
   ``` 
 
-  The meaning is as follows :
+  This means :
-  the circle is made from a point `base` together with an edge `loop`,
+  `S¹` is made from a point `base` and an edge `loop`,
-  so a map out of it to a space is the same as choosing
+  so a map out of `S¹` to a space is the same as choosing
   a point and an edge to map `base` and `loop` to respectively.
   Since `loop` is a path from `base` to itself,
   its image must also be a path from the image of `base` to itself.
@@ -85,5 +89,7 @@ define `doubleCover`.
   We want to map `loop` to `flipPath`,
   so `loop i` should map to a generic point in the path `flipPath`. 
   Try filling the hole.
+- Once you think you are done, reload the `agda` file with `C-c C-l`
+  and if it doesn't complain this means there are no problems with your definition.
 
 Defining `flipPath` is quite involved and we will do so in the next quest!

1FundamentalGroup/Quest0Part2.md

@@ -1,4 +1,4 @@
-# `refl ≡ loop` is empty - Defining `flipPath` via Univalence
+# `Refl ≡ loop` is empty - Defining `flipPath` via Univalence
 
 In this part, we will define the path `flipPath : Bool ≡ Bool`.
 Recall the picture of `doubleCover`.
@@ -12,13 +12,13 @@ We proceed in steps :
 
 1. Define the function `Flip : Bool → Bool`.
 2. Promote this to an isomorphism `flipIso : Bool ≅ Bool`.
-3. The intuition is that the univalence axiom asserts that
+3. We use _univalence_ to turn `flipIso` into 
-   paths in the space of spaces correspond to
+   a path `flipPath : Bool ≡ Bool`.
+   The univalence axiom asserts that
+   paths in `Type` - the space of spaces - correspond to
    homotopy-equivalences of spaces.
    As a corollary,
-   we can make paths in `Type` from isomorphisms of types.
+   we can make paths in `Type` from isomorphisms in `Type`.
-   We use this to turn `flipIso` into 
-   a path `flipPath : Bool ≡ Bool`.
 
 ## The function
 
@@ -29,18 +29,17 @@ We proceed in steps :
   Flip x = {!!}
   ```
 - Write `x` inside the hole,
-  and do `C-c C-c` with your cursor still inside.
+  and do `C-c C-c` with your cursor still inside. 
-  The `c` stands for _cases_.
   You should now see :
   ```agda
   Flip : Bool → Bool
   Flip false = {!!}
   Flip true = {!!} 
   ```
-  What this is saying is that 
+  This means : 
   the space `Bool` is made of two points `false, true` and nothing else,
-  so to map out of it, 
+  so to map out of `Bool` it suffices 
-  it suffices to give something to map `false` and `true` to respectively.
+  to find images for `false` and `true` respectively.
 - Since we want `Flip` to flip `true` and `false`,
   fill the first hole with `true` and the second with `false`.
 - To check things have worked,
@@ -57,7 +56,7 @@ We proceed in steps :
   This means `agda` recognises `Flip` as a well-formulated term
   and is a point in the space of maps from `Bool` to `Bool`.
 - We can also ask `agda` to compute outputs of `Flip`.
-  Try `C-c C-n`. (`n` stands for _normalise_.)
+  Try `C-c C-n` (`n` stands for _normalise_),
   `agda` should again be asking for an expression.
   Enter `Flip true`.
   In the `*Agda Information*` window, you should see `false`, as desired.
@@ -75,10 +74,10 @@ We proceed in steps :
   flipIso : Bool ≅ Bool
   flipIso = iso {!!} {!!} {!!} {!!}  
   ```
-- Check that what `agda` is expecting in the first two holes
+- Check that `agda` expects functions `Bool → Bool` 
-  are functions `Bool → Bool`.
+  to go in the first two holes.
-  These are our maps back and forth which will constitute the isomorphism
+  These are the maps back and forth which constitute the isomorphism,
-  so write `Flip` and `Flip` in the first two holes.
+  so fill them with `Flip` and its inverse `Flip`.
 - Check the goal of the next two holes.
   They should be 
   ```agda
@@ -90,6 +89,7 @@ We proceed in steps :
   ```
   This means we need to prove
   `Flip` is a right inverse and a left inverse of `Flip`.
+
 - Write the following so that your code looks like 
   ```agda
   flipIso : Bool ≅ Bool 
@@ -104,6 +104,30 @@ We proceed in steps :
   The `where` allows you to make definitions local to the current definition,
   in the sense that you will not be able to access `s` and `r` outside this proof.
   Note that what follows `where` must be indented.
+  <p>
+  <details>
+  <summary>Skipped step</summary>
+
+- To find out why we put `s b` on the left you can try 
+  ```agda
+  flipIso : Bool ≅ Bool 
+  flipIso = iso Flip Flip s r where
+
+    s : section Flip Flip
+    s = {!!}
+    
+    r : retract Flip Flip
+    r = {!!} 
+  ```
+- Check the goal of the hole `s = {!!}` and try using `C-c C-r`.
+  It should give you `λ x → {!!}`.
+  This says it's asking for some new proof for each `x : Bool`.
+  If you check the goal you can find out what proof it wants
+  and that `x : Bool`.
+- To do a proof for each `x : Bool`, we can also just stick 
+  `x` before the `=` and do away with the `λ`.
+  </details>
+  </p>
 - Check the goal of the hole `s b = {!!}`.
   In the `*Agda Information*` window, you should see 
   ```agda
@@ -111,14 +135,20 @@ We proceed in steps :
   —————————————————————————————————
   b : Bool 
   ```
+  This says it suffices to find a path from `Flip (Flip b)` to `b`
+  in the space `Bool`.
   Try to prove this.
   <p>
   <details>
-  <summary>Hint</summary>
+  <summary>Tips</summary>
 
-  You need to do cases on what `b` can be.
+  You need to case on what `b` can be.
   Then for the case of `true` and `false`,
   try `C-c C-r` to see if `agda` can help.
+  
+  The added benefit of having `b` before the `=`
+  is exactly this - that we can case on what `b` can be.
+  This is called _pattern matching_.
   </details>
   </p>
 - Do the same for `r b = {!!}`.

1FundamentalGroup/Quest0Part3.md

@@ -1,23 +1,20 @@
-# `refl ≡ loop` is empty - transporting paths using the double cover
+# `refl ≡ loop` is empty - 'lifting' paths using the double cover
 
 By the end of this page we will have shown that 
-`refl ≡ loop` is an empty space,
+`refl ≡ loop` is an empty space.
-we start at the end, moving backwards to what we need,
+In `1FundamentalGroup/Quest0.agda` locate
-as we would often do in practice.
-
-In `Quest0.agda` you should see
 
 ```agda
 Refl≢loop : Refl ≡ loop → ⊥
 Refl≢loop h = ?
 ```
 
-In the library we have 
+The cubical library has the result 
 `true≢false : true ≡ false → ⊥`
 which says that the space of paths in `Bool`
 from `true` to `false` is empty.
-We will assume it here and leave it as a side quest,
+We will assume it here and leave the proof as a side quest,
-see `1FundamentalGroup/Quest0SideQuests/SideQuest0`.
+see `1FundamentalGroup/Quest0SideQuests/SideQuest1`.
 
 - Load the file with `C-c C-l` and navigate to the hole.
 - Write `true≢false` in the hole and refine using `C-c C-r`,
@@ -26,42 +23,54 @@ see `1FundamentalGroup/Quest0SideQuests/SideQuest0`.
 - Check the goal in the new hole using `C-c C-,`
   it should be asking for a path from `true` to `false`.
 
-To give this path we need to visualise 'lifting' `Refl` and `loop`
+To give this path we need to visualise 'lifting' `Refl`, `loop`
+and the homotopy `h : refl ≡ loop`
 along the Boolean-bundle `doubleCover`.
 When we 'lift' `Refl` - starting at the point `true : doubleCover base` -
 it will still be a constant path at `true`,
-which we can just draw as a dot `true`.
+drawn as a dot `true`.
 When we 'lift' `loop` - starting at the point `true : doubleCover base` -
 it will look like
 
  <!-- [insert picture] -->
 
-We can find the end points of both 'lifted paths' by using `subst`.
+The homotopy `h : refl ≡ loop` is 'lifted'
-We should be able to see that the end point of the 'lifted' 
+(starting at 'lifted `refl`')
-`Refl` is just `true` and the end point of the 'lifted' `loop` is `false`.
+to some kind of surface 
-Now a homotopy `h : refl ≡ loop` is 'lifted' to some kind of surface 
 
 <!-- [insert picture] -->
 
-The end points of each 'lifted paths' in the 'lifted homotopy' 
+According to the pictures the end point of the 'lifted' 
-form a path in the endpoint fiber `doubleCover base`
+`Refl` is `true` and the end point of the 'lifted' `loop` is `false`.
-from the endpoint of 'lifted `Refl`' to the endpoint of 'lifted `base`',
+We are interested in the end points of each 
-i.e. a path from `true` to `false` in `Bool`, which is what we need.
+'lifted paths' in the 'lifted homotopy',
+since this forms a path in the endpoint fiber `doubleCover base`
+from `true` to `false`
 
-We use `endPt` to pick out the end points of 'lifted paths', 
+<!-- [insert picture] -->
-given to us in the library (originally called `subst`):
+
+We can evaluate the end points of both 'lifted paths' by using 
+something in the cubical library called `endPt` 
+(originally called `subst`).
 
 ```agda
 endPt : (B : A → Type) (p : x ≡ y) (bx : B x) → B y
 ```
 
+<p>
+<details>
+<summary>Try interpreting what it says</summary>
+
 It says given a bundle `B` over space `A`, 
 a path `p` from `x : A` to `y : A`, and
 a point `bx` above `x`,
 we can get the end point of 'lifted `p` starting at `bx`'.
 So let's make the function that takes
 a path from `base` to `base` and spits out the end point 
-of the 'lifted path'.
+of the 'lifted path' starting at `true`.
+
+</details>
+</p>
 
 ```agda
 endPtOfTrue : (p : base ≡ base) → doubleCover base
@@ -70,8 +79,8 @@ endPtOfTrue p = ?
 
 Try filling in `endPtOfTrue` using `endPt` 
 and the skills you have developed so far.
-You can check that `endPtOfTrue Refl` is `true`
+You can verify our expectation that `endPtOfTrue Refl` is `true`
-and that `endPtOfTrue loop` is `false` using `C-c C-n`.
+and `endPtOfTrue loop` is `false` using `C-c C-n`.
 
 Lastly we need to make the function `endPtOfTrue`
 take the path `h : refl ≡ loop` to a path from `true` to `false`.
@@ -85,3 +94,5 @@ cong : (f : A → B) → (p : x ≡ y) → f x ≡ f y
 ```
 
 Using `cong` and `endPtOfTrue` you should be able to complete Quest0.
+If you have done everything correctly you can reload `agda` and see that
+you have no remaining goals.

EmacsCommands.md

@@ -13,11 +13,16 @@ Example `C-c C-l` in Agda files is `Ctrl-c`, let go, `Ctrl-l`
 
 ## General Doom Emacs usage
 
+The 'ambient mode' is called __evil mode_ and follows 
+vim-like bindings.
+The following commands are for _evil mode_:
+
 - `SPC h b b` to look for bindings
 - `SPC f f` to find files. can use `TAB` for auto-completing paths
 - `h j k l` for left down up right
 - `SPC b k` to kill 'buffers'
-- `i` to go into 'insert' and `ESC` or `C-g` to escape 'insert'.
+- `i` to go into __insert mode_ (in insert mode you can insert text)
+  and `ESC` or `C-g` to go back to _evil mode_.
 - `C-_` to undo
 
 For beta users, to get the latest patch
@@ -28,6 +33,7 @@ For beta users, to get the latest patch
 
 ## Agda usage
 
+To insert text in the `agda` file use `i` to enter _insert mode_. 
 
 - `C-c C-l` loads the file
 - `C-c C-,` checks goal of the hole your cursor is in.
@@ -37,5 +43,5 @@ For beta users, to get the latest patch
 - `C-c C-d` used for checking types of terms
 - `C-c C-n` used for 'reducing' terms to their 'simplest form'
 - `C-c C-.` does `C-c C-,` and `C-c C-d`
-
+- `M-SPC c d` looks up the definition of the thing you are hovering over.