# Quest 0 - Working with 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. You don’t need to know any prerequisites - in particular we will define the fundamental group and higher homotopy groups if you don’t know what they are already.

Important

In your cloned copy of the HoTT Game locate the file `1FundamentalGroup/Quest0.agda`, and open this file in `emacs`. Before starting it is important to have a look at our guide to emacs and list of emacs commands.

## Part 0 - The Circle

### Theory - Definition of the Circle

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`.

```data S¹ : Type where
base : S¹
loop : base ≡ base
``` • `S¹` is a point in `Type`, the space of spaces. In other words, `S¹` is a space.

• `base` is a point in the space `S¹`

• `loop` is a path in `S¹` from `base` to itself. This is phrased as saying `loop` is a point in `base ≡ base` the space of paths from `base` to `base`.

Path

We think of a path in a space `A` as consisting of its starting point, its end point, and some generic point in the middle agreeing on the boundary.

You can see this as defining the circle via a CW-complex.

Type theory notation

In general `a : A` is read as `a` is a point in the space `A`. Note that in the above definition `S¹` is seen both as a point and a space depending on the context. In `cubical agda`, everything is a point in a “unique” space.

Type theory notation

In general when `a b : A` (`a` and `b` are points in a space `A`), we have a path space `a ≡ b`, whose points are paths from `a` to `b` in the space `A`.

### Exercise - defining the constant path `Refl`

There are other paths in `S¹`, for example the constant path at `base`. In `1FundamentalGroup/Quest0.agda` navigate to

```Refl : base ≡ base
Refl = {!!}
```

We will guide you through defining it. We are about to construct a path `Refl : base ≡ base`, a path from `base` to `base`.

Tip

The `{!!}` are called holes. These are blanks in the `agda` file that you can fill to complete the quest. You can write `?` to make a new hole.

We will fill the hole `Refl = {!!}`.

• Make sure you are in insert mode by pressing `i`. To escape insert mode press `ESC`.

Note

We have compiled a list of useful `emacs` and `agda` commands in Emacs Commands.

• Enter `C-c C-l` (this means `Ctrl-c Ctrl-l`).

Whenever you do this, `agda` will check the document is written correctly.

We say `agda` compiles or loads the file. This will open the `*Agda Information*` window looking like

```?0 : base ≡ base
?1 : (something)
?2 : (something)
...
```

This is the list of unfilled holes that are in your file currently. You should see that the holes in the file have changed in appearance, for example :

```Refl : base ≡ base
Refl = { }0
```

These are what holes look like when the file is compiled. The numbering is just for reference and may change upon reloading.

• Navigate between holes using `C-c C-f` (forward) or `C-c C-b` (backward).

• Navigate to the first hole, making sure your cursor is inside the hole. Check the goal using `C-c C-,` (this means `Ctrl-c Ctrl-comma`). Whenever you do `C-c C-,`, `agda` will tell you what kind of “point” it expects in the hole. The `*Agda Information*` window should be focused on this hole only :

```Goal: base ≡ base
```

This says `agda` is expecting a path from `base` to `base` in the hole. Making sure your cursor is still inside the hole, 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 → {!!}`. This is the `agda` way of writing `i ↦ {!!}`. Load the file again (using `C-c C-l`) and the `*Agda Information*` window should now look like :

```?0 : S¹
...
?6 : (something)

———— Errors ———————————————
Failed to solve the following constraints:
?0 (i = i1) = base : S¹ (blocked on _3)
?0 (i = i0) = base : S¹ (blocked on _3)
```

Do not worry about the errors, we will soon explain it.

• Navigate (`C-c C-f` and `C-c C-b`) to that new hole in `λ i → {!!}` and enter `C-c C-,` to check the goal. The `*Agda information*` window should look like :

```Goal: S¹
—————————————————————————
i : I
———— Constraints ——————————————
?0 (i = i1) = base : S¹ (blocked on _3, belongs to problem 4)
?0 (i = i0) = base : S¹ (blocked on _3, belongs to problem 4)
_4 := λ i → ?0 (i = i) (blocked on problem 4)
```

This says :

• `agda` is expecting a point in `S¹` for this hole.

• you have a point `i` in `I` available to you. You can think of `I` as the “unit interval” and `i` as a generic point in the interval.

• The point in `S¹` that you give has to satisfy the constraints that it is `base` when “`i = 1`” and “`i = 0`”. In `agda`, `i0` and `i1` are the “start” and “end” point of `I`. Afterall, we are defining a path from `base` to itself.

• Don’t worry about the last line.

• Since `Refl` is meant to be the constant path at `base`, write `base` in the hole.

• 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.

Tip

Everytime you are filling a hole, it is recommended that you first write what you want to fill in the hole then do `C-c C-SPC`. You can do it in the reverse order, however the recommended order has other benefits down the line.

• Load the file again (`C-c C-l`). The `*Agda Information*` window should now look like this :

```?0 : Bool
?1 : Bool ≅ Bool
?2 : Bool ≡ Bool
?3 : Type
?4 : doubleCover base
?5 : ⊥
```

The `?0 : S¹` has disappeared. This means `agda` has accepted what you filled this hole with.

• If you want to play around with this you reset this question by replacing what you wrote with `?` and doing `C-c C-l`.

## Part 1 - `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.

Paths between paths

In general if we have `p q : a ≡ b` in a space `A` then a path `Path : p ≡ q` in the path space `a ≡ b` consists of

• the starting path `p`

• the end path `q`

• and some generic path in between `Path i : a ≡ b` that agrees on the boundary

In algebraic topology this is called a path homotopy.

First, we define the empty space and what it means for a space to be empty. Here is what this looks like in `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 Different notions of “empty”), however for our present purposes we will use the first definition. Our goal is therefore to produce a point in the function space

```( 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

We 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`. 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*.

Homotopy type theory

A path `p : X ≡ Y` between two spaces `X Y : Type` (viewed as points in the space of spaces) can be visualised as follows :

• Two spaces `X` and `Y` as end points.

• For the generic point `i : I` in the interval `p i : Type` is a space that varies continuously with to respect to `i` such that `p 0` is `X` and `p 1` is `Y`.

The continuity guarantees that each point along the path looks “the same”. In particular the end points look “the same”.

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`.

• Make sure you are in insert mode.

• Navigate to the definition of `doubleCover` and make sure you have loaded the file with `C-c C-l`.

```doubleCover : S¹ → Type
doubleCover x = {!!}
```
• Navigate to the hole and check the goal. It should look like

```Goal: Type
————————————————————
x : S¹
```

This says it is expecting a point in `Type`, the space of spaces, i.e. it expects a space. We will first case on x by writing `x` in the hole and doing `C-c C-c` (`c` for cases). You should now see two new holes :

```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 to map `base` to, and an edge to map `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.

• Navigate to the first new hole and check the goal. We want to map `base` to the space `Bool` so write `Bool` in the hole, then do `C-c C-SPC` to fill it.

• Navigate to the second new hole and check the goal. Here `loop i` is a generic point in the path `loop`, where `i : I` is a generic point of the “unit interval”. We are assuming we have `flipPath` defined already and want to map `loop` to `flipPath`, so `loop i` should map to a generic point in the path `flipPath`.

Note

We can use `flipPath` without completing the definition of `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. Compare your definition to that in `1FundamentalGroup/Quest0Solutions.agda` to check that your definition is the one we want. To navigate to solutions file escape insert mode using `ESC` and do `SPC f f` to find the file, see Emacs Commands. Here is a definition that `agda` will accept, but is not what we need:

```doubleCover : S¹ → Type
doubleCover base = Bool
doubleCover (loop i) = Bool
```

Defining `flipPath` is quite involved and we will do so in the following part.

## Part 2 - 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`.

### The function

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`.

Isomorphism

One with a topological mindset might worry if isomorphism means homeomorphism, homotopy equivalence, bijection or something else; one might even wonder what continuity is here. The answer is that this is synthetic homotopy theory, where

• there is no need for real numbers

• every map is continuous in the sense that they respect paths

• an isomorphism `A ≅ B` is given by the data of

• `fun : A → B`

• `inv : B → A`

• `rightInv` that says (extensionally) `fun ∘ inv` is homotopic to the identity, i.e. given any `b : B` we have a path `fun ∘ inv b ≡ b`.

• `leftInv` that says (extensionally) `inv ∘ fun` is homotopic to the identity.

You might notice that the above looks like the classical definition of homotopy equivalence. (They turn out to be “the same”.)

Univalence

We have described paths between points as giving a starting point, an ending point, and a generic point between that agrees on the boundary. Drawing a path between spaces in the space of spaces, we can see that such a path is the data of two spaces that “continuously look the same”:

We already have a notion of “the same” for spaces, which is isomorphism. Hence we assume the following “univalence” axiom : Any isomorphism can be turned into a path between spaces.

• In `1FundamentalGroup/Quest0.agda`, navigate to :

```Flip : Bool → Bool
Flip x = {!!}
```
• Make sure you are in insert mode.

• Check the goal. It should be asking for a point in `Bool`, since we have already given it an `x : Bool` at the front.

Tip

Whenever you encounter a new hole, you should first check the goal.

• Write `x` inside the hole, and case on `x` using `C-c C-c` with your cursor still inside. You should now see :

```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 its space). Then `agda` will ask you to input an expression. Enter `Flip`. In the `*Agda Information*` window, you should see

```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

```flipIso : Bool ≅ Bool
flipIso = {!!}
```
• Refine with `C-c C-r`. You should now see

```flipIso : Bool ≅ Bool
flipIso = iso {!!} {!!} {!!} {!!}
```
• Given two spaces `A` and `B`, `iso` (with respect to `A` and `B`) belongs to the following space :

```iso : (fun : A → B) (inv : B → A)
(rightInv : section fun inv) (leftInv : retract fun inv) →
A ≅ B
```

which says that `iso` will produce an isomorphism from `A` to `B` given a map `fun` forwards and an inverse `inv` backwards, and points of the space `section fun inv` and `retract fun inv`. Try to find out what `section` and `retract` are by doing `C-c C-n` and entering their respective names. They should respectively say that `inv` is a right and left inverse of `fun`.

• Check the first two holes, `agda` should expect functions `Bool → Bool` to go in both of them. This is because it is expecting a function and its inverse, respectively, so fill them with `Flip` and its inverse `Flip`.

• Check the goal of the next two holes. They should be

```section Flip Flip
```

and

```retract Flip Flip
```
• Add the following to your code (make sure you copy it exactly) :

```flipIso : Bool ≅ Bool
flipIso = iso Flip Flip {!!} {!!} where

rightInv : section Flip Flip
rightInv x = {!!}

leftInv : retract Flip Flip
leftInv x = {!!}
```

Then load the file with `C-c C-l`. If `agda` gives an error it could be due to

1. missing spaces; `agda` is space sensitive

2. wrong indentation before `rightInv` and `leftInv`; `agda` is intentation sensitive

3. missing the `where` in the second line.

4. lower and upper case differences

where to use `where`

The `where` allows you to make definitions local to the current definition, in the sense that you will not be able to access `rightInv` and `leftInv` outside this proof. We will eventually fill the missing holes from before with `rightInv` and `leftInv`. If you like you can also place the definitions of `rightInv` and `leftInv` before `flipIso`.

• Check the goal of the hole `rightInv x = {!!}`. In the `*Agda Information*` window, you should see

```Goal: Flip (Flip x) ≡ x
—————————————————————————————————
x : Bool
```

This says `rightInv` should give for each `x : Bool` a path `p : Flip (Flip x) ≡ x`. We gave an `x : Bool` in front, so the goal is simply to give a path `p : Flip (Flip x) ≡ x`. Try to give such a path.

Hint

You need to case on what `x` can be. Then for the case of `false`, `Flip (Flip false)` should just be `false` by design, so you need to give a path from `false` to `false`.

The benefit of having `x` before the `=` is that we can case on what `x` can be. This is called pattern matching.

• Do the same for `leftInv x = {!!}`.

• Fill in the missing goals from the original problem using `rightInv`, `leftInv`.

• If you got the definition right then `agda` should not have any errors when you load using `C-c C-l`.

### The path

• Navigate to

```flipPath : Bool ≡ Bool
flipPath = {!!}
```
• In the hole, write in `isoToPath` and refine with `C-c C-r`. You should now have

```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 to normalise `pathToFun flipPath false`. You should get `true` in the `*Agda Information*` window.

What `pathToFun` 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`! Try to follow what `pathToFun` does in the animation.

`pathToFun`

`pathToFun` is called `transport` in the cubical library.

## Part 3 - Lifting paths using `doubleCover`

By the end of this page we will have shown that `refl ≡ loop` is an empty space. In `1FundamentalGroup/Quest0.agda` locate

```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 Proving true≢false.

• Load the file with `C-c C-l` and navigate to the hole. Write `true≢false` (input `\==n` for `≢`; see Emacs Commands) 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 Bool-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`.

```endPt : (B : A → Type) (p : x ≡ y) (bx : B x) → B y
```

Note

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 paths” starting at `true`.

```endPtOfTrue : base ≡ base → doubleCover base
endPtOfTrue p = {!!}
```
• Check the goal. It should be asking for

```Goal: Bool
—————————————————————————─
p : base ≡ base
———— Constraints ———————————————
?0 (p = loop) = false : Bool
(blocked on _29, belongs to problem 90)
?0 (p = Refl) = true : Bool (blocked on _29, belongs to problem 90)
_40 := λ p i → endPtOfTrue (p i) (blocked on problem 90)
```
• We want to use `endPt`, which can output something in the space `B y` (as described above). In this case we want `B y` to be `Bool`. `agda` is smart and can figure out how to use `endPt` :

1. Type `endPt` into the hole and do `C-c C-r`.

Tip

In general if the goal of the hole

```Goal: Y
————————————————————————
f : X → Y
...
```

is to find a point in a space `Y` and you have a function `f : X → Y` then you can write `f` in the hole and do `C-c C-r`.

You should see

```endPtOfTrue : base ≡ base → doubleCover base
endPtOfTrue p = endPt {!!} {!!} {!!}
```
1. Try to fill in these holes.

• Once you think you are done, 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`.)

```cong : (f : A → B) → (p : x ≡ y) → f x ≡ f y
```

We will define `cong` in a side quest 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.