+
Viewing the picture vertically,
for each point `x : S¹`,
we call `doubleCover x` the _fiber of `doubleCover` over `x`_.
@@ -52,7 +57,11 @@ 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`.
diff --git a/1FundamentalGroup/Quest0Part2.md b/1FundamentalGroup/Quest0Part2.md
index 561d189..ecf93b2 100644
--- a/1FundamentalGroup/Quest0Part2.md
+++ b/1FundamentalGroup/Quest0Part2.md
@@ -2,7 +2,11 @@
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`
diff --git a/1FundamentalGroup/Quest0Part3.md b/1FundamentalGroup/Quest0Part3.md
index 865ca75..78aece5 100644
--- a/1FundamentalGroup/Quest0Part3.md
+++ b/1FundamentalGroup/Quest0Part3.md
@@ -32,26 +32,29 @@ drawn as a dot `true`.
When we 'lift' `loop` - starting at the point `true : doubleCover base` -
it will look like
-
+
The homotopy `h : Refl ≡ loop` is 'lifted'
(starting at 'lifted `Refl`')
to some kind of surface
-
+
According to the pictures the end point of the 'lifted'
`Refl` is `true` and the end point of the 'lifted' `loop` is `false`.
We are interested in the end points of each
'lifted paths' in the 'lifted homotopy',
since this forms a path in the endpoint fiber `doubleCover base`
-from `true` to `false`
-
-
+from `true` to `false`.
We can evaluate the end points of both 'lifted paths' by using
-something in the cubical library called `endPt`
-(originally called `subst`).
+something in the cubical library (called `subst`) which we call `endPt`.
```agda
endPt : (B : A → Type) (p : x ≡ y) (bx : B x) → B y
@@ -93,6 +96,6 @@ from `f x` to `f y`.
cong : (f : A → B) → (p : x ≡ y) → f x ≡ f y
```
-Using `cong` and `endPtOfTrue` you should be able to complete Quest0.
+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.
diff --git a/1FundamentalGroup/Quest1.agda b/1FundamentalGroup/Quest1.agda
new file mode 100644
index 0000000..1a7bf8e
--- /dev/null
+++ b/1FundamentalGroup/Quest1.agda
@@ -0,0 +1,16 @@
+module 1FundamentalGroup.Quest1 where
+
+open import Cubical.Core.Everything
+open import Cubical.HITs.S1
+open import Cubical.Data.Nat
+open import Cubical.Data.Int
+open import Cubical.Foundations.Prelude
+
+Ω : (A : Type) (a : A) → Type
+Ω A a = a ≡ a
+
+loop_times : ℤ → Ω S¹ base
+loop pos zero times = refl
+loop pos (suc n) times = loop pos n times ∙ loop
+loop negsuc zero times = sym loop
+loop negsuc (suc n) times = loop negsuc n times ∙ sym loop
diff --git a/1FundamentalGroup/Quest1Part0.md b/1FundamentalGroup/Quest1Part0.md
index 54ba15f..ec5d6ed 100644
--- a/1FundamentalGroup/Quest1Part0.md
+++ b/1FundamentalGroup/Quest1Part0.md
@@ -19,6 +19,81 @@ In general the _loop space_ of a space `A` at a point `a` is defined as follows
Ω A a = a ≡ a
```
+Clearly for each integer `n : ℤ` we have a path
+that is '`loop` around `n` times'.
+Locate `loop_times` in the `Quest1.agda`
+(note how `agda` treats underscores)
+
+```agda
+loop_times : ℤ → Ω S¹ base
+loop n times = {!!}
+```
+
+Try casing on `n`, you should see
+
+```agda
+loop_times : ℤ → Ω S¹ base
+loop pos n times = {!!}
+loop negsuc n times = {!!}
+```
+
+It says to map out of `ℤ` it suffices to
+map the non-negative integers (`pos`)
+and the negative integers (`negsuc`).
+
+```agda
+data ℤ : Type where
+ pos : (n : ℕ) → ℤ
+ negsuc : (n : ℕ) → ℤ
+```
+
+This definition of `ℤ` uses the naturals, so try
+casing on `n` again, you should see
+
+```agda
+loop_times : ℤ → Ω S¹ base
+loop pos zero times = {!!}
+loop pos (suc n) times = {!!}
+loop negsuc n times = {!!}
+```
+
+It says to map out of `ℕ` it suffices to map `zero` and
+map each succesive integer `suc n` inductively.
+When we loop `zero` (`pos zero`) times what should we get?
+Try filling it in.
+For looping `pos (suc n)` times we loop `n` times and
+loop once more.
+For this we need composition of paths.
+
+```agda
+_∙_ : x ≡ y → y ≡ z → x ≡ z
+```
+
+Try typing `_∙_` or `? ∙ ?` in the hole (input `/.`)
+and refining.
+Checking the new holes you should see that now you need
+to give two loops.
+Try giving it '`loop n times`' composed with `loop`.
+Then try to also define the map on the negative integers.
+You will need to invert paths using `sym`.
+
+
+Looking up definitions
+
+If you don't know the definition of something
+you can look up the definition by sticking your cursor
+on it and pressing `M-SPC c d` in _insert mode_
+or `SPC c d` in _evil mode_.
+
+You can use it to find out the definition of `ℤ` and `ℕ`.
+
+
+
+Let's be more precise about homotopical data :
+We can check that a space is 'homotopically trivial' (h-trivial)
+from dimension `n`
+by checking if spheres of dimension `n` can be filled.
+To be h-trivial from `0` is for any two points
+to have a line in between; to fill `S⁰`.
+This data is captured in
+
+```agda
+isProp : Type → Type
+isProp A = (x y : A) → x ≡ y
+```
+
+
+All maps are continuous in HoTT
+
+There is a subtlety in the definition `isProp`.
+This is _stronger_ than saying that the space `A` is path connected.
+Since `A` is equipped with a continuous map taking pairs `x y : A`
+to a path between them.
+
+We will show that `isProp S¹` is _empty_ despite `S¹` being path connected.
+
+