Added Quest0Part2.md, Quest0Part3.md

1FundamentalGroup/Quest0.agda

@@ -3,14 +3,10 @@ module 1FundamentalGroup.Quest0 where
 open import Cubical.Data.Empty
 open import Cubical.Data.Unit renaming ( Unit to ⊤ )
 open import Cubical.Data.Bool
-open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Prelude renaming ( subst to endPt )
 open import Cubical.Foundations.Isomorphism renaming ( Iso to _≅_ )
 open import Cubical.Foundations.Path
 
-private
-  variable
-    u : Level
-
 data S¹ : Type where
   base : S¹
   loop : base ≡ base
@@ -18,33 +14,21 @@ data S¹ : Type where
 Refl : base ≡ base
 Refl = λ i → base
 
+{- transport
+
+To follow a point in `a : A` along a path `p : A ≡ B`
+we use
+
+  transport : {A B : Type u} → A ≡ B → A → B
+
+Why do we propify? Discuss.
+
+-}
+
 Flip : Bool → Bool
 Flip false = true
 Flip true = false
 
-{- Iso
-
-We show that Flip is an isomorphism from Bool → Bool
-with inverse Flip.
-
-A proof of `A ≅ B` (input \cong or write Iso A B) is given by
-
-  iso f i s r
-
-where
-
-  f : A → B and i : B → A
-
-are the map and its inverse,
-here both `f` and `i` are Flip
-
-`s` is a proof that `f` is a section with
-right inverse `i` and
-`r` is a proof that `f` is a retraction
-with left inverse `i`
-
--}
-
 flipIso : Bool ≅ Bool
 flipIso = iso Flip Flip s r where
   s : section Flip Flip
@@ -55,30 +39,9 @@ flipIso = iso Flip Flip s r where
   r false = refl
   r true = refl
 
-{- Path ≡
-
-A corollary of univalence is
-`isoToPath` which takes an isomorphism
-`f : A ≅ B` and gives a path
-`fPath : A ≡ B`.
-The resulting path has the important property
-that when you follow (transport/subst)
-a point in `A` along the path
-you will get the point `f(a)` in `B`
-
--}
-
 flipPath : Bool ≡ Bool
 flipPath = isoToPath flipIso
 
-{-
-
-Try out `transport` on `true : Bool` and
-`flipPath` by doing `C-c C-n`
-and typing in `transport flipPath true`
-
--}
-
 {- bundle over S¹
 
 We want to construct a bundle over S¹
@@ -117,8 +80,8 @@ Note that `doubleCover base` is just `Bool` (externally).
 
 -}
 
-SubstTrue : (p : base ≡ base) → doubleCover base
-SubstTrue p = subst doubleCover p true
+endPtOfTrue : (p : base ≡ base) → doubleCover base
+endPtOfTrue p = endPt doubleCover p true
 
 {-
 
@@ -145,4 +108,4 @@ by
 -}
 
 refl≢loop : refl ≡ loop → ⊥
-refl≢loop p = true≢false (cong SubstTrue p)
+refl≢loop p = true≢false (cong endPtOfTrue p)

1FundamentalGroup/Quest0Part0.md

@@ -86,3 +86,4 @@ We will fill the hole `{ }0`.
 - 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/Quest0Part2.md

@@ -0,0 +1,155 @@
+# `refl ≡ loop` is empty - Defining `flipPath` via Univalence
+
+In this part, we will define the path `flipPath : Bool ≡ Bool`.
+Recall the picture of `doubleCover`.
+(Insert gif.)
+
+This means we need `flipPath` to correspond to 
+the unique non-identity permutation of `Bool`
+that flips `true` and `false`.
+
+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
+   paths in the space of spaces correspond to
+   homotopy-equivalences of spaces.
+   As a corollary,
+   we can make paths in `Type` from isomorphisms of types.
+   We use this to turn `flipIso` into 
+   a path `flipPath : Bool ≡ Bool`.
+
+## The function
+
+- In `1FundamentalGroup/Quest0.agda`, navigate to :
+
+  ```agda
+  Flip : Bool → Bool
+  Flip x = {!!}
+  ```
+- Write `x` inside the hole,
+  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 
+  the space `Bool` is made of two points `false, true` and nothing else,
+  so to map out of it, 
+  it suffices to give something to map `false` and `true` to 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,
+  try `C-c C-d`. (`d` stands for _deduce_.)
+  Then `agda` will ask you to input an expression.
+  Enter `Flip`.
+  In the `*Agda Information*` window,
+  you should see 
+
+  ```agda
+  Bool → Bool  
+  ```
+  
+  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_.)
+  `agda` should again be asking for an expression.
+  Enter `Flip true`.
+  In the `*Agda Information*` window, you should see `false`, as desired.
+
+## The isomorphism
+
+- Navigate to
+  ```agda
+  flipIso : Bool ≅ Bool
+  flipIso = {!!} 
+  ```
+- Write `iso` in the hole and refine with `C-c C-r`.
+  You should now see 
+  ```agda
+  flipIso : Bool ≅ Bool
+  flipIso = iso {!!} {!!} {!!} {!!}  
+  ```
+- Check that what `agda` is expecting in the first two holes
+  are functions `Bool → Bool`.
+  These are our maps back and forth which will constitute the isomorphism
+  so write `Flip` and `Flip` in the first two holes.
+- Check the goal of the next two holes.
+  They should be 
+  ```agda
+  section Flip Flip 
+  ```
+  and 
+  ```agda
+  retract Flip Flip 
+  ```
+  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 
+  flipIso = iso Flip Flip s r where
+
+    s : section Flip Flip
+    s b = {!!}
+    
+    r : retract Flip Flip
+    r b = {!!} 
+  ```
+  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.
+- Check the goal of the hole `s b = {!!}`.
+  In the `*Agda Information*` window, you should see 
+  ```agda
+  Goal: Flip (Flip b) ≡ b
+  —————————————————————————————————
+  b : Bool 
+  ```
+  Try to prove this.
+  <p>
+  <details>
+  <summary>Hint</summary>
+
+  You need to do cases on what `b` can be.
+  Then for the case of `true` and `false`,
+  try `C-c C-r` to see if `agda` can help.
+  </details>
+  </p>
+- Do the same for `r b = {!!}`.
+- Use `C-c C-d` to check that `agda` is okay with `flipIso`.
+
+## The path
+
+- Navigate to 
+  ```agda
+  flipPath : Bool ≡ Bool
+  flipPath = {!!} 
+  ```
+- In the hole, write in `isoToPath` and refine with `C-c C-r`.
+  You should now have 
+  ```agda
+  flipPath : Bool ≡ Bool
+  flipPath = isoToPath {!!} 
+  ```
+  If you check the new hole, you should see that
+  `agda` is expecting an isomorphism `Bool ≅ Bool`.
+  
+  `isoToPath` is the function from the cubical library
+  that converts isomorphisms between spaces
+  into paths between the corresponding points in the space of spaces `Type`.
+- Fill in the hole with `flipIso`
+  and use `C-c C-d` to check `agda` is happy with `flipPath`.
+- Try `C-c C-n` with `transport flipPath false`.
+  You should get `true` in the `*Agda Information*` window.
+  
+  What `transport` did is it took the path `flipPath` in the 
+  space of spaces `Type` and followed the point `false`
+  as `Bool` is transformed along `flipPath`.
+  The end result is of course `true`,
+  since `flipPath` is the path obtained from `flip`!

1FundamentalGroup/Quest0Part3.md

@@ -0,0 +1,87 @@
+# `refl ≡ loop` is empty - transporting paths using the double cover
+
+By the end of this page we will have shown that 
+`refl ≡ loop` is an empty space,
+we start at the end, moving backwards to what we need,
+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 
+`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,
+see `1FundamentalGroup/Quest0SideQuests/SideQuest0`.
+
+- 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`,
+  `agda` knows `true≢false` maps to `⊥` so it automatically
+  will make a new hole.
+- 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`
+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`.
+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`.
+We should be able to see that the end point of the 'lifted' 
+`Refl` is just `true` and the end point of the 'lifted' `loop` is `false`.
+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' 
+form a path in the endpoint fiber `doubleCover base`
+from the endpoint of 'lifted `Refl`' to the endpoint of 'lifted `base`',
+i.e. a path from `true` to `false` in `Bool`, which is what we need.
+
+We use `endPt` to pick out the end points of 'lifted paths', 
+given to us in the library (originally called `subst`):
+
+```agda
+endPt : (B : A → Type) (p : x ≡ y) (bx : B x) → B y
+```
+
+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'.
+
+```agda
+endPtOfTrue : (p : base ≡ base) → doubleCover base
+endPtOfTrue p = ?
+```
+
+Try filling in `endPtOfTrue` using `endPt` 
+and the skills you have developed so far.
+You can check that `endPtOfTrue Refl` is `true`
+and that `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`.
+In general if `f : A → B` is a function and `p` is a path
+between points `x y : A` then we get a map `cong f p`
+from `f x` to `f y`.
+(Note that `p` here is actually a homotopy `h`.)
+
+```agda
+cong : (f : A → B) → (p : x ≡ y) → f x ≡ f y
+```
+
+Using `cong` and `endPtOfTrue` you should be able to complete Quest0.