Quest 1 - Loop Space of the Circle

Part 0 - Definition of the Loop Space

In this quest, we continue to formalise the problem statement.

The problem statement

The fundamental group of S¹ is ℤ.

Intuitively, the fundamental group of S¹ at base 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 :

loopSpace : (A : Type) (a : A) → Type
loopSpace A a = a ≡ a

For now, we will treat the loop space of S¹ as the fundamental group. Later we will understand why this is illegal in general (the fundamental group is set truncated) but legitimate in this special case (the loop space of S¹ turns out to be a set anyway).

Exercise - `loop_times`

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)

loop_times : ℤ → loopSpace S¹ base
loop n times = {!!}

Note

You can use underscores when you name a function. agda will put the inputs in the underscores in order.

Try casing on n, you should see

loop_times : ℤ → loopSpace 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). The definition of ℤ in agda is

data ℤ : Type where
  pos    : ℕ → ℤ
  negsuc : ℕ → ℤ

It says is ℤ is two copies of ℕ where the first copy represents 0, 1, 2, ..., and the second represents -1, -2, ... (negsuc n is meant to mean - (n + 1)). This definition of ℤ uses the naturals, so try casing on n again, you should see

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 successive integer suc n inductively. We can do the same with negsuc n, obtaining four cases.

loop_times : ℤ → Ω S¹ base
loop pos zero times = {!!}
loop pos (suc n) times = {!!}
loop negsuc zero times = {!!}
loop negsuc (suc n) times = {!!}

These four cases represent :

If you “loop 0 times” then you stay at base.
If you “loop n + 1 times”, you “loop n times” then “loop once more”.
If you “loop -1 times”, you “loop once in reverse”
If you “loop -(n + 2) times”, you loop “loop -(n + 1) times” then “loop once more in reverse”

Individually

Try filling the first hole with what we get when we loop 0 (pos zero) times.
For looping pos (suc n) times we loop n times and loop once more. For this we need composition of paths.
```
_∙_ : 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.
```
loop pos (suc n) times = {!!} ∙ {!!}
```
Try giving it “loop n times” concatenated with loop.
To “loop in reverse” we use
```
sym : x ≡ y → y ≡ x
```
Use this to define “loop -1 times”.
For the last case “concatenate loop -(n + 1) times with loop in reverse”.

Part 1 - Making a Path From `ℤ` to Itself

In the previous part 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 (Refl is now refl which is more general) from loop, the idea is to replace Bool with ℤ, allowing us to distinguish between all loops on S¹. In this quest we will construct one of the two comparison maps across the whole circle, called windingNumber.

The plan is :

Define a function sucℤ : ℤ → ℤ that increases every integer by one
Prove that sucℤ is an isomorphism by constructing an inverse map predℤ : ℤ → ℤ.
Turn the isomorphism sucℤ into a path sucℤPath : ℤ ≡ ℤ using isoToPath
Define helix : S¹ → Type by mapping base to ℤ and a generic point loop i to sucℤPath i.
Use helix and endPt to define the map windingNumberBase : base ≡ base → ℤ. Intuitively it counts how many times a path loops around S¹. a generic point loop i to sucℤPath i.
Generalize this across the circle.

In this part, we focus on 1, 2 and 3.

Defining `sucℤ`

Set up the definition of sucℤ so that it is of the form :
```
Name : TypeOfSpace
Name inputs = ?
```
Just writing in the name and the type of the space is enough for now. Load the file and check that it is looks like:
Solution:
```
sucℤ : ℤ → ℤ
sucℤ = ?
```
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 :
Solution:
```
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 :
```
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 zero to pos zero. 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ℤ (negsuc zero) computes to pos zero and sucℤ (pos zero) computes to pos (suc zero).

`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 section sucℤ predℤ and retract sucℤ predℤ.

`sucℤ` is a Path

Imitating what we did with flipPath, upgrade sucℤIso to sucℤPath.

Part 2 - Winding Number

The `ℤ`-bundle `helix`

We want to make a ℤ-bundle over S¹ by ‘copying ℤ across the loop via sucℤPath’. In Quest1.agda locate

helix : S¹ → Type
helix = {!!}

Try to imitate the definition of doubleCover to define the bundle helix. You should compare your definition to ours in Quest1Solutions.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

windingNumberBase : base ≡ base → helix base
windingNumberBase = {!!}

Hint

endPt evaluates the end point of ‘lifted paths’.

Try computing a few values using C-c C-n, you can try it on refl, loop, ‘loop three times’, ‘loop negative one times’ and so on.

Generalising

The function windingNumberBase can actually be improved without any extra work to a function on all of S¹.

windingNumber : (x : S¹) → base ≡ x → helix x
windingNumber = {!!}

Try filling this in. 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 ℤ.

Quest 1 - Loop Space of the Circle

Part 0 - Definition of the Loop Space

Exercise - loop_times

Part 1 - Making a Path From ℤ to Itself

Defining sucℤ

sucℤ is an Isomorphism

sucℤ is a Path