# Quest 3 - The Loop Space is `ℤ`

In Quest 1 - Loop Space of the Circle we introduced our main method of proving that the fundamental group (which we take to be `loopSpace S¹ base` for now) is `ℤ`, and in Quest 2 - ℤ is a Set we decided that this means to show that they are equal spaces. .. admonition:: The Goal

```loopSpace≡ℤ : loopSpace S¹ base ≡ ℤ
loopSpace≡Z = {!!}
```

As usual we will show this via giving an isomorphism, so we must make comparison maps forward and back. However, we discovered we had to define the backwards map over all of `S¹`. We already have `windingNumber`, the forwards comparison map, which gives us a map `loopSpace S¹ base → ℤ` when applied to `base`.

```windingNumber : (x : S¹) → base ≡ x → helix x
```

In this quest our goal is to make a map backwards

Current Goal

```rewind : (x : S¹) → helix x → base ≡ x
```

Since `windingNumber` took a path and found how many times the path loops around, in general “an integer twisted around the helix a bit”, or “an integer plus a bit”. We want to make `rewind` do the reverse. So `rewind` should take “an integer `n` plus a bit”, loop around `n` times, then add that extra corresponding bit, the path from `base` to `x` to the end.

## Part 0 - `rewind`

### Dependent paths

We try making `rewind`. We can assume a point `x : S¹`, then case on what it is.

```rewind : (x : S¹) → helix x → base ≡ x
rewind base = {!!}
rewind (loop i) = {!!}
```

In the case of `base` we want a map from `helix base` i.e. `ℤ`, to `base ≡ base`. Try filling this in.

Solution

We want this to be the correct inverse, described as looping around `n` times and adding that extra bit on the end. However there is nothing to add at the end in this case, so it should just be `loop_times`, which we already defined in Quest 1 - Loop Space of the Circle.

The case of `loop i` will be a lot more work. Checking the goal we see that at each point `loop i` on the loop, it wants a point in the space `helix (loop i) → base ≡ (loop i)`, which it might reduce to `sucℤPath i → base ≡ (loop i)` according to the definition of `helix`.

Collecting these spaces together along this `i`, we obtain a loop in the space of spaces based at the space `ℤ → base ≡ base` given by

```λ i → helix (loop i) → base ≡ (loop i) : (ℤ → base ≡ base) ≡ (ℤ → base ≡ base).
```

Now collecting the points we need to give into a “path” as well, we obtain the notion of a dependent path : each point of this “path” belongs to a space along the path of spaces. We define dependent paths and design a way of mapping out of `S¹` in general in Quest 5 - Dependent Paths from Trinitarianism. We assume from now on knowledge of dependent paths.

### Using `outOfS¹`

Now that we have a way of mapping out of `S¹` (using `PathD`), called `outOfS¹D`, try to use it to repackage the work we have to far.

Solution

Originally we have

```rewind : (x : S¹) → helix x → base ≡ x
rewind base = loop_times
rewind (loop i) = {!!}
```

Now we rearrange this to

```rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times {!!}
```

since our bundle over `S¹` is `(λ x → helix x → base ≡ x)` and our image for `base` is `loop_times`.

Checking the last goal, it remains to give a dependent path of type `PathD (λ i → sucℤPath i → base ≡ loop i) loop_times loop_times`. Remembering the definition of `PathD`, this should be exactly giving a path `pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times ≡ loop_times`, since `PathD` reduces the issue of dependent paths to just paths in the end space, which is `ℤ → base ≡ base` in this case. Let’s make this a chain of equalities :

Solution
```rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ {!!} ⟩
loop_times ∎
)
```

### Functions and `pathToFun`

The map `loop_times` takes an integer and does `loop` that many times. On the other hand `pathToFun` follows how `loop_times` changed along the path of spaces `λ i → sucℤPath i → base ≡ loop i`, and spits out the corresponding point at the end. This path of spaces is specifically a path of function spaces, so we need to find a more explicit way of describing what `pathToFun` does to spaces of functions.

To generalize, suppose we have spaces `A0 A1 B0 B1 : Type` and paths `A : A0 ≡ A1` and `B : B0 ≡ B1`. Then let `pAB` denote the path `λ i → A i → B i : (A0 → B0) ≡ (A1 → B1)`. We want to figure out what `pathToFun` does when it follows a function `f : A0 → B0` along the path `pAB`.

We know by functional extensionality that the function `pathToFun pAB f : A1 → B1` should be determined by what it does to terms in `A1`, so we can assume `a1 : A1`. The idea is we “apply `f` by sending `a1` back to `A0`”. Since `pathToFun (sym A) a1` is meant to give the point in `A0` that “looks like `a1`”, we try applying `f` to this point, then send it across again via the path `B` to the point `f (pathToFun (sym A) a1)` looks like in `B1`. We expect the outcome to be the same.

```pathToFun→ : {A0 A1 B0 B1 : Type} {A : A0 ≡ A1} {B : B0 ≡ B1} (f : A0 → B0) →
pathToFun (λ i → A i → B i) f ≡ λ a1 → pathToFun B (f (pathToFun (sym A) a1))
```

The proof of this in `cubical agda` is simply `refl`, so we need not even extract it as a lemma.

A cubical hack

Is actually one of the axioms asserted in `cubical agda` that `pathToFun (λ i → A i → B i) f` is externally equal to `λ a1 → pathToFun B (f (pathToFun (sym A) a1))`. Here we are using the `cubical` definition of `pathToFun` so we can simply give `refl` for its proof.

However, according the definition of `pathToFun` we gave in Trinitarianism, they are not externally equal but can be shown to be internally equal using `J`. We prove this from our own definitions here.

We interpret what this result means in our specific case : We are making `pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times` into another map in the space `ℤ → base ≡ base`, by following along the diagram

Specifically, this map should take `n : ℤ` and first send it backwards along `sucℤPath`, supposedly giving us `n - 1`. Then it applies `loop_times`, obtaining the loop `loop (n - 1) times`. Lastly it follows `loop (n - 1) times` along the path `λ i → base ≡ loop i` (which itself is a loop starting and ending at `base ≡ base` in the space of spaces), obtaining some path from `base ≡ base`, which we expect to be internally equal to `loop n times`.

Try putting this together in our definition of `rewind`, as a new intermediate step in our chain of equalities.

Solution
```rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ {!!} ⟩
loop_times ∎
)
```

We can simplify the above expression. We know that `pathToFun (sym sucℤPath) n` should follow `n` along `sucℤPath` backwards, so it should be `n - 1`. We can use this to move a step closer to the goal.

Solution

This equality is definitional.

```rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ refl ⟩
(λ n → pathToFun (λ i → base ≡ loop i) (loop (predℤ n) times))
≡⟨ {!!} ⟩
loop_times ∎
)
```

### The path fibration and `pathToFun`

It remains to find out how `pathToFun` interacts with the path of loops coming out of base. We call “the path of loops coming out of base” `λ i → base ≡ loop i` the path fibration at `base`. The animation tells us that we are gradually concatenating the input `loop (n - 1) times` with `loop`. Hence we should obtain `loop (n - 1) times ∙ loop`. We are a bit lucky here, and these are in fact definitionally equal, but to justify this in general, we can prove that “following along the path fibration is the same as concatenating”.

```pathToFunPathFibration : {A : Type} {x y z : A} (q : x ≡ y) (p : y ≡ z) →
pathToFun (λ i → x ≡ p i) q ≡ q ∙ p
```

This is in fact a quick exercise.

Hint

We take the propositional perspective - without loss of generality we can assume `y` and `z` are exactly the same.

Crucially : we know what `pathToFun` does to `refl` (recall `pathToFunRefl` from the quest on paths).

Solution
```pathToFunPathFibration : {A : Type} {x y z : A} (q : x ≡ y) (p : y ≡ z) →
pathToFun (λ i → x ≡ p i) q ≡ q ∙ p
pathToFunPathFibration {A} {x} {y} q = J (λ z p → pathToFun (λ i → x ≡ p i) q ≡ q ∙ p)
(
pathToFun refl q
≡⟨ pathToFunRefl q ⟩
q
≡⟨ ∙Refl q ⟩
q ∙ refl ∎
)
```

To include this in `rewind` we have

Spoiler
```rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩ -- how pathToFun interacts with →
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ refl ⟩ -- sucℤPath is just taking successor, and so its inverse is definitionally taking predecessor
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (predℤ n)))
≡⟨ funExt (λ n → pathToFunPathFibration _ _) ⟩ -- how pathToFun interacts with the "path fibration"
(λ n → (loop (predℤ n) times) ∙ loop)
≡⟨ {!!} ⟩
loop_times ∎
)
```

There are several ways to complete this final part. We will leave the rest in a hint.

Hint

Applying functional extensionality we just need to show that for each `n : ℤ` the outputs are equal, i.e. `loop predℤ n times ∙ loop ≡ loop n times`. By our design of `loop_times` we should have that `loop m times ∙ loop` is equal to `loop (m + 1) times`. Then we are reduced to showing that `loop (sucℤ predℤ n) times ≡ loop n times`, or just `sucℤ predℤ n ≡ n`.

Solution
```rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩ -- how pathToFun interacts with →
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ refl ⟩ -- sucℤPath is just taking successor, and so its inverse is definitionally taking predecessor
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (predℤ n)))
≡⟨ funExt (λ n → pathToFunPathFibration _ _) ⟩ -- how pathToFun interacts with the "path fibration"
(λ n → (loop (predℤ n) times) ∙ loop)
≡⟨ funExt (λ n →
loop predℤ n times ∙ loop
≡⟨ loopSucℤtimes (predℤ n) ⟩
loop (sucℤ (predℤ n)) times
≡⟨ cong loop_times (sucℤPredℤ n) ⟩
loop n times ∎) ⟩
loop_times ∎
)
```

We can check that `rewind base` is indeed `loop_times` by using `C-c C-n`. This is to be expected as `outOfS¹` evaluated at `base` should back exactly what we fed it, as mentioned in the discussion on mapping out of the circle.

## Part 1 - `rewind` is a right inverse

We are now in a position to approach the main goal :

```loopSpaceS¹≡ℤ : loopSpace S¹ base ≡ ℤ
loopSpaceS¹≡ℤ = {!!}
```

We have reduced this to giving an isomorphism, which involves giving the map `windingNumber base` forward and `loop_times` backwards, and showing that they are inverses of each other.

Hence the next step is to show that “looping `n` times then taking the winding number gives back `n`”. Try to state and prove this in `1FundamentalGroup/Quest3.agda`. In the hints we will use intuitive notation for integers that may not align exactly with `agda` code.

The statement
```windingNumberRewindBase : (n : ℤ) → windingNumber base (rewind base n) ≡ n
windingNumberRewindBase = {!!}
```

We identify `rewind base` with `loop_times`, since they are externally equal.

Hint 0

Since `loop_times` was defined by casing on `n` we case on `n` - it could be zero, a positive integer, negative one, or less than negative one.

Hint 1

Some of the cases are trivial - we know exactly what `loop 0 times` and `windingNumber base loop` are.

Solution for Hint 1
```windingNumberRewindBase : (n : ℤ) → windingNumber base (rewind base n) ≡ n
windingNumberRewindBase (pos zero) = refl
windingNumberRewindBase (pos (suc n)) = {!!}
windingNumberRewindBase (negsuc zero) = refl
windingNumberRewindBase (negsuc (suc n)) = {!!}
```

Hint 2

We can identify `windingNumber base` with its definition, reducing the problem to showing that `endPt helix (loop n times) 0` is equal to `n`, in the separate cases.

For the first case, we can reduce `loop (n + 1) times` to just `loop n times ∙ loop` since that was the definition. Hence we are interested in what `endPt helix (loop n times ∙ loop) 0` is. Recalling our intuition behind `endPt`, this amounts to following the point `0` up the `helix` along the path `loop n times ∙ loop`. This should just be going to `endPt helix (loop n times) 0` then adding `1`.

You can also check what `agda` reduces the expression to by writing it in the hole and then doing `C-c C-n`. It should look something like `sucℤ (transp (λ i → helix (loop pos n times i)) i0 (pos 0))`. Clearly it has reduced the definition a bit too far, but the important idea is there, that it is `+ 1` of whatever data we have already.

Lastly we can just take `sucℤ` on both sides of an equality we have from the induction hypothesis.

Solution

For one of the cases we detail the thought process going on above, and for the last case we extract only the important part of the proof.

```windingNumberRewindBase : (n : ℤ) → windingNumber base (rewind base n) ≡ n
windingNumberRewindBase (pos zero) = refl
windingNumberRewindBase (pos (suc n)) =
windingNumber base (rewind base (pos (suc n)))
≡⟨ refl ⟩
windingNumber base (loop (pos n) times ∙ loop)
≡⟨ refl ⟩
endPt helix (loop (pos n) times ∙ loop) (pos zero)
≡⟨ refl ⟩
sucℤ (endPt helix (loop (pos n) times) (pos zero))
≡⟨ cong sucℤ (windingNumberRewindBase (pos n)) ⟩
sucℤ (pos n)
≡⟨ refl ⟩
pos (suc n) ∎
windingNumberRewindBase (negsuc zero) = refl
windingNumberRewindBase (negsuc (suc n)) = cong predℤ (windingNumberRewindBase (negsuc n))
```

You might wonder if it is possible to make the above map work across all of `S¹`, and the answer is yes. This is not really necessary for our goal, so feel free to skip to the next part if you are not interested. Try stating and proving the generalization of the above; which we call `windingNumberRewind`.

The Statement
```windingNumberRewind : (x : S¹) (n : helix x) → windingNumber x (rewind x n) ≡ n
windingNumberRewind = {!!}
```

Hint 0

We defined `rewind` by casing on points in the circle and `rewind` is the first function being applied, so it would make sense to case on points in the circle. In the case when the point is `base` we can just give the map we wanted to generalize in the first place.

Solution to Hint 0
```windingNumberRewind : (x : S¹) (n : helix x) → windingNumber x (rewind x n) ≡ n
windingNumberRewind =
outOfS¹D (λ x → (n : helix x) → windingNumber x (rewind x n) ≡ n)
windingNumberRewindBase {!!}
```

Hint 1

Checking the last hole we see that we need to give a dependent path from `windingNumberRewindBase` to itself. According to the definition of a dependent path, this is just a path in the last fiber from `pathToFun` of `windingNumberRewindBase` to `windingNumberRewindBase` (the fiber is `(n : ℤ) → windingNumber base (rewind base n) ≡ n`). Now this might seem very complicated : even after applying functional extensionality (this is equality of two functions) this would be “finding a path between paths in `ℤ`”. Try repeating that last bit in your head a couple of times.

Hint 2

We put a lot of effort into showing that `ℤ` is a set.

Solution
```windingNumberRewind : (x : S¹) (n : helix x) → windingNumber x (rewind x n) ≡ n
windingNumberRewind = -- must case on x / use recursor / outOfS¹ since that is def of rewind
outOfS¹D (λ x → (n : helix x) → windingNumber x (rewind x n) ≡ n)
windingNumberRewindBase (
pathToFun
(λ i → (n : helix (loop i)) → windingNumber (loop i) (rewind (loop i) n) ≡ n)
windingNumberRewindBase
≡⟨ funExt (λ x → isSetℤ _ _ _ _ ) ⟩
windingNumberRewindBase ∎)
```

## Part 2 - `rewind` is a left inverse

Try to show that `rewind` is a left inverse.

The Statement

Just like we struggled to only define `windingNumber base` without access to the entire circle, we make sure to include all the data we have access to. Note that this was not the case before.

```rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = {!!}
```

Hint 0

Remembering that `windingNumber x p` is externally equal to `endPt helix p 0`, and that `endPt` is defined by path induction - using `J` (this is not exactly true for `endPt` from the library for `cubical` reasons), the obvious thing to do here is to do path induction.

Solution for Hint 0
```rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p) {!!}
```

Hint 1

It suffices to show that `rewind x (windingNumber x refl) ≡ refl`, which by reducing the left side is the same as showing `loop_times (endPt helix refl 0) ≡ refl`.

Solution to Hint 1
```rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p)
(rewind base (windingNumber base refl)
≡⟨ refl ⟩
loop_times (endPt helix (refl {x = base}) (pos zero))
≡⟨ {!!} ⟩
refl ∎)
```

Hint 2

We know what `endPt` does to `refl`, which is given by the result `endPtRefl`. If you need to recall what `endPtRefl` proves you can type it into the hole and do `C-c C-.` for the goal and the type of `endPtRefl`.

Solution to Hint 2
```rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p)
(rewind base (windingNumber base refl)
≡⟨ refl ⟩
loop_times (endPt helix (refl {x = base}) (pos zero))
≡⟨ cong loop_times (cong (λ g → g (pos zero)) (endPtRefl {x = base} helix)) ⟩
loop (pos zero) times
≡⟨ {!!} ⟩
refl ∎)
```

Solution

The last step is simply remembering how `loop_times` computes.

```rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p)
(rewind base (windingNumber base refl)
≡⟨ refl ⟩
loop_times (endPt helix (refl {x = base}) (pos zero)) -- reduce both definitions
≡⟨ cong loop_times (cong (λ g → g (pos zero)) (endPtRefl {x = base} helix)) ⟩
loop (pos zero) times
≡⟨ refl ⟩
refl ∎)
```

## Part 3 - The Loop Space is `ℤ`

We can conclude our main goal now, by collecting all of the components we have made above. We leave you the pleasure.

Solution

As usual we construct an isomorphism, but we can choose to do this over the entire circle or just between `loopSpace S¹ base` and `ℤ`. We do the former and have the latter as a corollary, but you could just do the latter directly as well.

```pathFibration≡helix : (x : S¹) → (base ≡ x) ≡ helix x
pathFibration≡helix x =
isoToPath (iso (windingNumber x) (rewind x) (windingNumberRewind x) (rewindWindingNumber x))

loopSpaceS¹≡ℤ : loopSpace S¹ base ≡ ℤ
loopSpaceS¹≡ℤ = pathFibration≡helix base
```

### What now?

We have mentioned already that we aren’t exactly working with the fundamental group, but the loop space. In the final quest of this arc we discuss the definition of the fundamental group and show that the loop space in this case is the fundamental group already.