diff --git a/1FundamentalGroup/Quest0Part0.md b/1FundamentalGroup/Quest0Part0.md
deleted file mode 100644
index d2cb5ca..0000000
--- a/1FundamentalGroup/Quest0Part0.md
+++ /dev/null
@@ -1,118 +0,0 @@
-The Circle
-=======================
-
-In this series of quests we will prove that the fundamental group
-of `S¹` is `ℤ`.
-In fact, our strategy will also show that the higher homotopy groups of
-`S¹` are all trivial.
-We begin by formalising the problem statement.
-
-A contruction of 'the circle' is :
-
-- a point called `base`
-- an edge from that point to itself called `loop`
-
-Here is our definition of the circle in `agda`.
-
-```agda
-data S¹ : Type where
- base : S¹
- loop : base ≡ base
-```
-
-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.
-
-
-
-Further details
-
-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
-
-
-
-
-An "edge" is the same as a path.
-There are other paths in `S¹`,
-for example the _constant path at `base`_.
-In `1FundamentalGroup/Quest0.agda` naviage to
-
-```agda
-Refl : base ≡ base
-Refl = {!!}
-```
-
-we will guide you through defining it.
-We are about to construct a path `Refl : base ≡ base`
-(read path `Refl` from `base` to `base`)
-The _hole_ `{ }0` is where you describe the path.
-We will fill the hole `{ }0`.
-
-- enter `C-c C-l` (this means `Ctrl-c Ctrl-l`).
- Whenever you do this, `agda` will check the document is written correctly.
- This will open the `*Agda Information*` window looking like
-
- ```
- ?0 : base ≡ base
- ?1 : (something)
- ?2 : (something)
- ...
- ```
-
- This says you have some unfilled _holes_.
-- navigate to the hole `{ }0` using `C-c C-f` (forward) or `C-c C-b` (backward)
-- enter `C-c C-r`. The `r` stands for _refine_.
- Whenever you do this whilst having your cursor in a hole,
- Agda will try to help you.
-- you should now see `λ i → { }1`.
- This is `agda` suggesting that for each
- `i : I` (if you like you can think of this as a generic point
- on the the unit interval `I`)
- you give a point in between the start and end of the path.
- This is all you need to specify a path in `agda`.
-- navigate to that new hole
-- enter `C-c C-,` (this means `Ctrl-c Ctrl-comma`).
- Whenever you make this command whilst having your cursor in a hole,
- `agda` will check the _goal_, i.e. what kind of thing you need to stick in.
-- the goal (`*Agda information*` window) should look like
-
-```
- Goal: S¹
- —————————————————————————
- i : I
- ———— Constraints ——————————————
-...
-```
- you see that `agda` knows you have a generic point
- `i : I` on the unit interval.
- All the constraints are saying that when you look
- at `i = 0` and `i = 1`, whatever you give in between must
- match up with the end points of the path,
- namely `base` and `base`
-- write `base` in the hole, since this is the constant path
-- press `C-c C-SPC` to fill the hole with `base`.
- In general when you have some text (and your cursor) in a hole,
- doing `C-c C-SPC` will tell `agda` to replace the hole with that text.
- `agda` will give you an error if it can't make sense of your text.
-- 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`
-
diff --git a/1FundamentalGroup/Quest0Part1.md b/1FundamentalGroup/Quest0Part1.md
deleted file mode 100644
index f8bb909..0000000
--- a/1FundamentalGroup/Quest0Part1.md
+++ /dev/null
@@ -1,104 +0,0 @@
-# `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` :
-
-```agda
-data ⊥ : Type where
-```
-
-This says "the empty space `⊥` is a space with no points in it".
-
-Here are three candidate definitions for a space `A` to be empty :
-
-- 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` from `A` to the empty space
-- there is an isomorphism `i : A ≅ ⊥` of spaces
-
-These turn out to be 'the same' (see `1FundamentalGroup/Quest0SideQuests/SideQuest0`),
-however for our present purposes we will use the first definition.
-Our goal is therefore to produce a point in the function space
-
-```agda
-( Refl ≡ loop ) → ⊥
-```
-
-The authors of this series have thought long and hard
-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 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 ) → ⊥`.
-
-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.
-
-
-
-Viewing the picture vertically,
-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
-
-
-
-Let's assume for the moment that we have `flipPath` already and
-define `doubleCover`.
-
-- Navigate to the definition of `doubleCover` and make sure
- you have loaded the file with `C-c C-l`.
- ```agda
- doubleCover : S¹ → Type
- doubleCover x = {!!}
- ```
-- 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
- doubleCover : S¹ → Type
- doubleCover base = {!!}
- doubleCover (loop i) = {!!}
- ```
-
- This means :
- `S¹` is made from a point `base` and an edge `loop`,
- 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.
-- Use `C-c C-f` and/or `C-c C-b` to navigate to the first hole.
- We want to map `base` to `Bool` so
- fill the hole with `Bool` using `C-c C-SPC`.
-- Navigate to the second hole.
- Here `loop i` is a generic point in the path `loop`,
- where `i : I` is a generic point of the 'unit interval'.
- 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!
diff --git a/1FundamentalGroup/Quest0Part2.md b/1FundamentalGroup/Quest0Part2.md
deleted file mode 100644
index f910c1c..0000000
--- a/1FundamentalGroup/Quest0Part2.md
+++ /dev/null
@@ -1,187 +0,0 @@
-# `Refl ≡ loop` is empty - Defining `flipPath` via Univalence
-
-In this part, we will define the path `flipPath : Bool ≡ Bool`.
-Recall the picture of `doubleCover`.
-
-
-
-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. We use _univalence_ to turn `flipIso` into
- 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 in `Type`.
-
-## 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.
- You should now see :
- ```agda
- Flip : Bool → Bool
- Flip false = {!!}
- Flip true = {!!}
- ```
- This means :
- the space `Bool` is made of two points `false, true` and nothing else,
- so to map out of `Bool` it suffices
- 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,
- 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 `agda` expects functions `Bool → Bool`
- to go in the first two holes.
- These are the maps back and forth which constitute the isomorphism,
- so fill them with `Flip` and its inverse `Flip`.
-- 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.
-
-
- Skipped step
-
- - 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 `λ`.
-
-
-- 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.
-
-
- Tips
-
- 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_.
-
-
-- 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`!
diff --git a/1FundamentalGroup/Quest0Part3.md b/1FundamentalGroup/Quest0Part3.md
deleted file mode 100644
index b5da7c3..0000000
--- a/1FundamentalGroup/Quest0Part3.md
+++ /dev/null
@@ -1,101 +0,0 @@
-# `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.
-In `1FundamentalGroup/Quest0.agda` locate
-
-```agda
-Refl≢loop : Refl ≡ loop → ⊥
-Refl≢loop h = ?
-```
-
-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 the proof as a side quest,
-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`,
- `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`, `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`,
-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`.
-
-We can evaluate the end points of both 'lifted paths' by using
-something in the cubical library (called `subst`) which we call `endPt`.
-
-```agda
-endPt : (B : A → Type) (p : x ≡ y) (bx : B x) → B y
-```
-
-
-
-Try interpreting what it says
-
-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' starting at `true`.
-
-
-
-
-```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 verify our expectation that `endPtOfTrue Refl` is `true`
-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`.
-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`.
-If you have done everything correctly you can reload `agda` and see that
-you have no remaining goals.
diff --git a/1FundamentalGroup/Quest1Part0.md b/1FundamentalGroup/Quest1Part0.md
deleted file mode 100644
index 28cc407..0000000
--- a/1FundamentalGroup/Quest1Part0.md
+++ /dev/null
@@ -1,97 +0,0 @@
-# Loop Space
-
-In this quest,
-we continue to formalise the problem statement.
-
-> The fundamental group of `S¹` is `ℤ`.
-
-Intuitively,
-the fundamental group of `S¹` at `base` is
-consists of loops based as `base` up to homotopy of paths.
-In homotopy type theory,
-we have a native description of loops based at `base` :
-it is the space `base ≡ base`.
-
-In general the _loop space_ of a space `A` at a point `a` is defined as follows :
-
-```agda
-Ω : (A : Type) (a : A) → Type
-Ω A a = a ≡ a
-```
-
-Clearly for each integer `n : ℤ` we have a path
-that is '`loop` around `n` times'.
-Locate `loop_times` in `1FundamentalGroup/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`.
-
-```agda
-sym : x ≡ y → y ≡ x
-```
-
-
-
-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 `ℕ`.
-
-
-
-
diff --git a/1FundamentalGroup/Quest1Part1.md b/1FundamentalGroup/Quest1Part1.md
deleted file mode 100644
index b0d4482..0000000
--- a/1FundamentalGroup/Quest1Part1.md
+++ /dev/null
@@ -1,129 +0,0 @@
-# Homotopy Levels
-
-The loop space can contain higher homotopical information that
-the fundamental group does not capture.
-For example, consider `S²`.
-
-```agda
-data S² : Type where
- base : S²
- loop : base ≡ base
- northHemisphere : loop ≡ refl
- southHemisphere : refl ≡ loop
-```
-
-
-
-What is `refl`?
-
-For any space `A` and point `a : A`,
-`refl` is the constant path at `a`.
-Technically speaking, we should write `refl a` to indicate the point we are at,
-however `agda` is often smart enough to figure that out.
-
-
-
-Intuitively, all loops in `S²` based at `base` is homotopic to
-the constant path `refl`.
-In other words, the fundamental group at `base` of `S²` is trivial.
-However, the 'composition' of the path `southHemisphere` with `northHemisphere`
-in `base ≡ base` gives the surface of `S²`,
-which intuitively is not homotopic to the constant point `base`.
-So `base ≡ base` has non-trivial path structure.
-
-
-
-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.
-
-
-
-
-Similarly, to be h-trivial from dimension `1` is for any two points `x y : A`
-and any two paths `p q : x ≡ y` to have a homotopy from `p` to `q`;
-to fill `S¹`. This is captured in
-
-```agda
-isSet : Type → Type
-isSet A = (x y : A) → isProp (x ≡ y)
-```
-
-To define the fundamental group we will make the loop space satisfy
-`isSet` by _trucating_ the loop space'.
-First we show that `isProp S¹` and `isSet S¹` are both empty.
-Locate `¬isSetS¹` in `1FundamentalGroup/Quest1.agda`.
-In the cubical library we have the result
-
-```agda
-isProp→isSet : (A : Type) → isProp A → isSet A
-```
-
-which we will not prove.
-Assuming `¬isSetS¹`, use `isProp→isSet` to deduce `¬isPropS¹`.
-
-
-
-
-
-HLevel
-
-Generalisation to HLevel and isHLevel n → isHLevel suc n??
-
-
-
-
-Turning our attention to `¬isSetS¹`,
-again given `h : isSet S¹` -
-a map continuously taking each pair `x y : A`
-to a point in `isProp (x ≡ y)`.
-We can apply `h` twice to the only point `base` available to us,
-obtaining a point of `isProp (base ≡ base)`.
-Try mapping from this into the empty space.
-
-
-
-Hint 0
-
-We have already shown that `Refl ≡ loop` is the empty space.
-We have imported `Quest0Solutions.agda` for you,
-so you can just quote the result from there.
-
-
-
-
-
-
-Hint 1
-
-- assume `h`
-- type `Refl≢loop` it in the hole and refine
-- it should now be asking for a proof that `Refl ≡ loop`
-- try to use `h`
-
-
-
-
diff --git a/1FundamentalGroup/Quest1Part2.md b/1FundamentalGroup/Quest1Part2.md
deleted file mode 100644
index 4e847b3..0000000
--- a/1FundamentalGroup/Quest1Part2.md
+++ /dev/null
@@ -1,3 +0,0 @@
-# Set Truncation and Higher Homotopy Groups
-
-We've seen what it means for a space to be a "set".
diff --git a/1FundamentalGroup/Quest2Part0.md b/1FundamentalGroup/Quest2Part0.md
deleted file mode 100644
index b5a9de2..0000000
--- a/1FundamentalGroup/Quest2Part0.md
+++ /dev/null
@@ -1,101 +0,0 @@
-# Comparison maps between `Ω S¹ base` and `ℤ`
-
-In `Quest1` we have defined the map `loop_times : ℤ → Ω S¹ base`.
-Creating the inverse map is difficult without access to the entire circle.
-Similarly to how we used `doubleCover` to distinguish `refl` and `base`,
-the idea is to replace `Bool` with `ℤ`,
-allowing us to distinguish between all loops on `S¹`.
-In `Part0` and `Part1` we will construct one of the two comparison maps
-across the whole circle, called `spinCount`.
-
-The plan is :
-
-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`.
-<<<<<<< HEAD
-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`.
-=======
-5. Use `helix` and `endPt` to define the map
- `spinCountBase : base ≡ base → ℤ`
- Intuitively it counts how many times a path loops around `S¹`.
- a generic point `loop i` to `sucPath i`.
-6. Generalize this across the circle.
-
-In this part, we focus on `1`, `2` and `3`.
->>>>>>> df5d7c381b1adae1d2547df95f5d73bcf3447ac4
-
-## `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.
-
-
- Hint
-
- Do `C-c C-c` on `n`.
- Then map `negsuc 0` to `pos 0`.
- For `negsuc (suc n)`, map it to `negsuc n`.
-
-
-
-- 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
-<<<<<<< HEAD
- `section sucℤ predℤ` and `retract sucℤ predℤ`.
-=======
- `section sucℤ predℤ` and `retract sucℤ predℤ`.
-
-## `sucℤ` is a path
-
-- Imitating what we did with `flipPath`,
- upgrade `sucℤIso` to `sucℤPath`.
->>>>>>> df5d7c381b1adae1d2547df95f5d73bcf3447ac4
diff --git a/1FundamentalGroup/Quest2Part1.md b/1FundamentalGroup/Quest2Part1.md
deleted file mode 100644
index 97397ce..0000000
--- a/1FundamentalGroup/Quest2Part1.md
+++ /dev/null
@@ -1,54 +0,0 @@
-# Comparison maps between `Ω S¹ base` and `ℤ` - `spinCount`
-
-## The `ℤ`-bundle `helix`
-
-We want to make a `ℤ`-bundle over `S¹` by
-'copying ℤ across the loop via `sucℤPath`'.
-In `Quest2.agda` locate
-
-```agda
-helix : S¹ → Type
-helix = {!!}
-```
-
-Try to imitate the definition of `doubleCover` to define the bunlde `helix`.
-You should compare your definition to ours in `Quest2Solutions.agda`.
-Note that we have called this `helix`, since the picture of this `ℤ`-bundle
-looks like
-
-
-
-## Counting loops
-
-Now we can do what was originally difficult - constructing an inverse map
-(over all points).
-Now we want to be able to count how many times a path `base ≡ base` loops around
-`S¹`, which we can do now using `helix` and finding end points of 'lifted' paths.
-For example the path `loop` should loop around once,
-counted by looking at the end point of 'lifted' `loop`, starting at `0`.
-Hence try to define
-
-```agda
-spinCountBase : base ≡ base → helix base
-spinCountBase = {!!}
-```
-
-Try computing a few values using `C-c C-n`,
-you can try it on `refl`, `loop`, `loop 3 times`, `loop (- 1) times` and so on.
-
-## Generalising
-
-The function `spinCountBase`
-can actually be improved without any extra work to a function on all of `S¹`
-
-```agda
-spinCount : (x : S¹) → base ≡ x → helix x
-spinCount = {!!}
-```
-
-We will show that this and a general version of `loop_times` are
-inverses of each other over `S¹`, in particular obtaining an isomorphism
-between `base ≡ base` and `ℤ`.
diff --git a/1FundamentalGroup/feedbackG.md b/1FundamentalGroup/feedbackG.md
deleted file mode 100644
index 9825375..0000000
--- a/1FundamentalGroup/feedbackG.md
+++ /dev/null
@@ -1,44 +0,0 @@
-# George feedback
-
-## Subject info
-
-[] has some experience with type theory and haskell
-
-## Quest0/Part0
-
-[x] clarify the notation `a : A`
-[x] hide the imports
-[x] definition of inductive type doesn't make sense
- without the further details.
-[x] confusion of `{!!}` and `{0}` and `?`
-[x] comparing holes to agda-info window is intuitive
-[x] error on firsts refine
-[x] add at each step what the agda-info window looks like
-[x] confusion about hole numbers. "just ignore them"
-[x] subject tries to read constraint in agda-info window.
- Shld deal with this somehow.
-[] emphasize no need to fill holes in order.
-
-## Quest0/Part1
-
-[x] subject confused about 'space of spaces'.
- More specifically, need to say `a : A` means "`a` is a point of the space `A`".
-[x] we shld say `a ≡ b` means space of paths from `a` to `b`.
-[-] 'contradiction' is a pre-existing concept in subject brain.
-[x] "not sure that helps" - subject about definition of `Bool`
-[x] "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.
-[x] need to be clear _we are assuming `flipPath` is constructed already_.
-[x] overall : need to be clearer that `Type` is space of spaces,
- and paths in `Type` are saying which spaces are the same.
-
-## Quest0/Part2
-
-[x] For the `iso` bit, change to just `C-c C-r` cuz `Iso` only has one constructor.
-[x] say you can check def of `Iso` by using `SPC c d`
-[x] say "just write `s` and `r` and write the rest then load".
-[x] emphasize agda is indentation sensitive.
-[x] subject unexpectedly extracts lemma `true ≡ true`.
diff --git a/1FundamentalGroup/pi1S1.md b/1FundamentalGroup/pi1S1.md
deleted file mode 100644
index 44db99a..0000000
--- a/1FundamentalGroup/pi1S1.md
+++ /dev/null
@@ -1,33 +0,0 @@
-Fundamental Group of S¹
-================
-
-Prerequisites :
-- circle
-- loop space
-- have useless maps pi(S¹) → ℤ and ℤ → pi(S¹)
-
-
-
-
-- we make helix from ℤ ≡ ℤ
-
--
-
-Motivating Steps :
-0. After sufficient pondering, you guess that
- loops are determined by how many times they go around
-1. Count number of times loops go around using ℤ
- by setting the single loop to +1.
-2. You can make a comparison maps between loop space and ℤ
- but can't yet show an equivalence
-3. You realize you need to use the definition of S¹,
- so you go from `base ≡ base ≃ Z` to `base ≡ x ≃ Bundle x`.
- i.e. You try to make the equivalence _over_ S¹
-
-
-Random thought :
-to prove `a = b`, we realise that `a = f(x0)`
-and `b = g(x0)` for `x0 : X`,
-and instead show `(x : X) → f x = g x`.
-This turns out to be easier since we now get
-access to the recursor of `X`.