From d3e5063e5fbbe064c2aaf85ba6787f33d3dc1d52 Mon Sep 17 00:00:00 2001
From: Jlh18 <josephhua73@yahoo.com>
Date: Thu, 16 Sep 2021 12:24:04 +0100
Subject: [PATCH] edit 1FundamentalGroup/Quest0Part2

---
 1FundamentalGroup/Quest0Part2.md | 34 +++++++++++++++-----------------
 1 file changed, 16 insertions(+), 18 deletions(-)

diff --git a/1FundamentalGroup/Quest0Part2.md b/1FundamentalGroup/Quest0Part2.md
index a06c71e..561d189 100644
--- a/1FundamentalGroup/Quest0Part2.md
+++ b/1FundamentalGroup/Quest0Part2.md
@@ -108,24 +108,24 @@ We proceed in steps :
   <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
+  - 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 = {!!}
+      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 `λ`.
+      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 = {!!}`.
@@ -135,8 +135,6 @@ 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>