# Quest 2 - `ℤ` is a Set

An overview of this quest :

• We want to show that the higher loop spaces of `S¹` are trivial

• We note that it suffices to show that the loop space of `ℤ` is trivial, assuming the end result `loopSpace S¹ base ≡ ℤ`.

• Show that the loop space of any set is trivial, hence it suffices to show that `ℤ` is a set

• Show that `ℤ` looks like the sum of two disjoint copies of `ℕ`, and `ℕ` is a set; it then suffices to show the general result that the disjoint sum of two sets is a set.

• To show that the disjoint sum of sets is a set we find ourselves trying to classify the path space of disjoint sums.

The bulk of the work will be to classify the path space of disjoint sums, and showing that it actually corresponds to the path space. This is the content of the last three parts.

## Part 0 - `loopSpace loopSpace`

We are interested in knowing what the higher homotopy groups of `S¹` might be. Whilst the data of the fundamental group `π₁ S¹` is captured in `loopSpace S¹ base`, the data of `π₂ S¹` would be captured in `loopSpace (loopSpace S¹ base) refl`; loops in `loopSpace S¹ base` based at `refl`. Points in the second loop space are paths `h : refl ≡ refl`, i.e. `h` would be a homotopy from the constant path to itself.

The second loop space contains an obvious point `refl : refl ≡ refl` (this is of course not the same “refl” as the one before), and we could define the next loop space to be loops in `loopSpace (loopSpace S¹ base) refl` based at `refl` (the one from `loopSpace S¹ base` that is).

The important conclusion we will arrive at in this quest is that the loop space of `ℤ` - which will correspond to the second loop space of `S¹` (this is the conclusion of this entire arc) - is trivial, in the sense that it just consists of a point (up to paths) :

```loopSpace (loopSpace S¹ base) refl ≡ loopSpace ℤ 0 ≡ ⊤
```

Intuitively this is because the only loop (up to a path) in `ℤ` from `0` to itself is `refl`, so `loopSpace ℤ 0` is contractible - it looks just like the singleton space `⊤`. This is more general : any two paths in `ℤ` are homotopic, which we formalise in the definition `isSet`.

### `isSet`

`isSet`

The statement “any two paths in the space `A` are homotopic” is captured in the definition of `isSet` :

```isSet : Type → Type
isSet A = (x y : A) → isProp (x ≡ y)
```

In the above `isProp` captures the statement “any two points are (continuously) connected by a path” :

```isProp : Type → Type
isProp A = (x y : A) → x ≡ y
```

If a type satisfies `isSet` we say it is a set, and if it satisfies `isProp` we say it is a proposition.

Why the words "set" and "proposition"?

Intuitively a “set” is meant to be a bunch of disjoint points. However in homotopy type theory we consider points up to paths, and paths up to homotopy, hence a “set” is a bunch of disjoint blobs, where each blob is contractible to a point. In other words a “set” is a type where any circle (that lands in a blob) can be filled (hence the blob is contractible).

We will justify the use of the word “proposition” once we have introduced the propositional perspective on types, see trinitarianism and Part 5 - Using the Propositional Perspective.

All maps are continuous in HoTT

There is a subtlety in the definition `isProp`. Having `isProp A` 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 in a later quest that `isProp S¹` is empty despite `S¹` being path connected.

We can justify “the loop space of a set is trivial” by showing that “if any two paths in a space `A` are homotopic then the loop space of `A` at any point in `A` looks like `⊤`”. So we show that

```isSet→LoopSpace≡⊤ : {A : Type} (x : A) → isSet A → (x ≡ x) ≡ ⊤
isSet→LoopSpace≡⊤ = {!!}
```

Locate this in `1FundamentalGroup/Quest2.agda` and try filling it in.

Hint 0

Imitating what we did with `flipPath` and `flipIso` reduce this to showing that for each `x : A` and `h : isSet A` we have

• `fun : x ≡ x → ⊤`

• `inv : ⊤ → x ≡ x`

• `rightInv : section fun inv`

• `leftInv : retract inv fun`

Hint 1

There is only one possible map from `x ≡ x` to `⊤` since `⊤` is terminal (see trinitarianism).

To map out of `⊤` one can do cases and see that you only need to map `tt`.

Solution
• `fun` can just be `(λ p → tt)`

• `inv` can be

```inv : ⊤ → x ≡ x
inv tt = refl
```

Hint 2

For `rightInv` by casing on the point in `⊤` there should be nothing much to show.

For `leftInv` we need to use our assumption that “any two paths are homotopic”.

Solution
```rightInv : section (λ p → tt) inv
rightInv tt = refl

leftInv : retract (λ p → tt) inv
leftInv p = h x x refl p
```

The goal

We have therefore reduced our goal to showing that `ℤ` is a set, i.e. `ℤ` only has trivial paths in it, which will tell us that the second loop (and in fact any higher loop space) of `S¹` is trivial.

## Part 1 - `ℤ` as a disjoint sum `ℕ ⊔ ℕ`

As a first step, we note that `ℤ` actually looks like two disjoint copies of `ℕ`, i.e. we have

```ℤ≡ℕ⊔ℕ : ℤ ≡ ℕ ⊔ ℕ
```

where we have the definition of the disjoint sum of two spaces as follows

```data _⊔_ (A B : Type) : Type where

inl : A → A ⊔ B
inr : B → A ⊔ B
```

It says there are two ways of making points in the space, taking them from `A` and taking them from `B`. Try proving `ℤ ≡ ℕ ⊔ ℕ` in `1FundamentalGroup/Quest2.agda`.

Hint

As in defining `flipPath` in quest 0 we first make an isomorphism and then convert it to a path/proof of equality. To make the isomorphism note that the definition of `ℤ` is already as “two copies of `ℕ`”, as described in quest 1.

If you have made the function and inverse appropriately, you should only need constant paths in the proofs that they satisfy `section` and `retract` respectively.

Solution
```ℤ≡ℕ⊔ℕ : ℤ ≡ ℕ ⊔ ℕ
ℤ≡ℕ⊔ℕ = isoToPath (iso fun inv rightInv leftInv) where

fun : ℤ → ℕ ⊔ ℕ
fun (pos n) = inl n
fun (negsuc n) = inr n

inv : ℕ ⊔ ℕ → ℤ
inv (inl n) = pos n
inv (inr n) = negsuc n

rightInv : section fun inv
rightInv (inl n) = refl
rightInv (inr n) = refl

leftInv : retract fun inv
leftInv (pos n) = refl
leftInv (negsuc n) = refl
```

We want to show that `ℤ` is a set, by using the path `ℤ≡ℕ⊔ℕ`. Intuitively if `ℕ` is a set then two disjoint copies of it should also be a set, (think about filling circles on the disjoint sum). Thus we can break down our goal into two :

Goal 1 : `ℕ` is a set

```isSetℕ : isSet ℕ
isSetℕ = {!!}
```

Goal 2

If `A` and `B` are both sets then `A ⊔ B` is also a set.

Goal 1 will be handled in a side quest. We focus on Goal 2 from now on.

## Part 2 - Disjoint Sum of Sets is a Set

Try formulating (but not proving) the result `isSet⊔`, which should say “if spaces `A` and `B` are both sets then so is their disjoint sum `A ⊔ B`”. This should be done in `1FundamentalGroup/Quest2.agda` where indicated.

Solution
```isSet⊔ : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔ = {!!}
```

Without proving this, we can use this to show `isSet (ℕ ⊔ ℕ)` using `isSetℕ : isSet ℕ`, which will be shown in a side quest. Then using either `pathToFun` or `endPt` you can show `isSet ℤ` from `isSet (ℕ ⊔ ℕ)`, using the path from `ℤ` to `ℕ ⊔ ℕ` we made earlier. Try to set up everything described in this paragraph where indicated in `1FundamentalGroup/Quest2.agda`.

Hint : The statement
```isSetℤ : isSet ℤ
```

Hint : following along paths

To use `pathToFun` you must figure out what path you are following and what point you are following the path along.

To use `endPt` you must figure out what bundle you are making, what the path in the base space is, and what point you are starting at in the first fiber.

Partial solutions

The point you need to follow in either case is the point in the space `isSet (ℕ ⊔ ℕ)` :

```isSetℤ : isSet ℤ
isSetℤ = pathToFun {!!} (isSet⊔ isSetℕ isSetℕ)

isSetℤ' : isSet ℤ
isSetℤ' = endPt {!!} {!!} (isSet⊔ isSetℕ isSetℕ)
```

Solutions
```isSetℤ : isSet ℤ
isSetℤ = pathToFun (cong isSet (sym ℤ≡ℕ⊔ℕ)) (isSet⊔ isSetℕ isSetℕ)

isSetℤ' : isSet ℤ
isSetℤ' = endPt (λ A → isSet A) (sym ℤ≡ℕ⊔ℕ) (isSet⊔ isSetℕ isSetℕ)
```

Refining issues

If you tried refining using `endPt` you may have been given 2 holes instead of 3. This is because `agda` had too many possible options when trying to match up the output of `endPt` and the goal. To add an extra hole simply add a `?` afterwards and reload.

Once this is complete we can go back and work on `isSet⊔`.

## Part 3 - Path Space of Disjoint Sums

### Motivation

• Locate your formulation of `isSet⊔`.

• We assume `hA : isSet A`, `hB : isSet B`, and points `x y : A ⊔ B`. Currently our code looks like

```isSet⊔ : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔ hA hB x y = {!!}
```
• Check the goal. It should be asking for a point in the space `isProp (x ≡ y)`.

We need to consider how to get information on the path space of `A ⊔ B` when our hypotheses are about the path spaces of `A` and `B` respectively. We could try to case on `x` and `y`.

• If `x` and `y` are “both from `A`”, i.e. of the form `inl ax` and `inl ay` for `ax ay : A`, then we need to find a point in `isProp (inl ax ≡ inl ay)`. This should be due to `hA`, which gives us `hA ax ay : isProp (ax ≡ ay)`. So somehow we need to identify the path spaces `inl ax ≡ inl ay` and `ax ≡ ay` (try to formalize this, though we are not expecting a solution here).

• If `x` and `y` are of the forms `inl ax` and `inr by` respectively for `ax : A` and `by : B` then intuitively the space `inl ax ≡ inr bx` should be empty, since the sum is disjoint (again we are not expecting a solution here).

• The other two cases are similar.

The conclusion is that we need some kind of classification of the path space of disjoint sums.

### Classifying the Path Space of Disjoint Sums

Path space of disjoint sums

A path in the the disjoint sum should just be a path in one of the two parts.

This says points from `A` cannot be confused with points from `B` or points in `A` that they were not already path connected to.

For now we leave `isSet⊔` alone and define a function `⊔NoConfusion` that takes two points in `A ⊔ B` and returns a space, which is meant to represent the path space in each case, as described in our motivation above. Try to formulate (but not fill in) this where indicated in `Quest2.agda`. It should look like:

Solution
```⊔NoConfusion : {A B : Type} → A ⊔ B → A ⊔ B → Type
⊔NoConfusion = {!!}
```

Assume points `x` and `y` in the disjoint sum and try to case on them. There should be four cases.

• When both points are from `A`, i.e. they are `inl ax` and `inl ay`, then we should give the space `ax ≡ ay`, which we expect to be isomorphic to `inl ax ≡ inl ay`.

• (Two cases) When each is from a different space we expect the path space between them to be empty, so we should give `⊥`.

• If both are from `B` then we should imitate what we did in the first case

Solution
```⊔NoConfusion : A ⊔ B → A ⊔ B → Type
⊔NoConfusion (inl x) (inl y) = x ≡ y -- Path A x y
⊔NoConfusion (inl x) (inr y) = ⊥
⊔NoConfusion (inr x) (inl y) = ⊥
⊔NoConfusion (inr x) (inr y) = x ≡ y -- Path B x y
```

### Using the Classification

Now we have two of goals :

• `Path≡⊔NoConfusion` : We need to show that for each `x y : A ⊔ B` the path space looks like our classification, i.e. that `(x ≡ y) ≡ (⊔NoConfusion x y)`

• `isSet⊔NoConfusion` : For `isSet⊔`, given `hA : isSet A`, `hB : isSet B` and `x y : A ⊔ B` we needed to show `isProp (x ≡ y)`. Hence we want to show that under the same assumptions `isProp (⊔NoConfusion x y)`.

Formalise (but don’t prove) both of these where indicated in `1FundamentalGroup/Quest2.agda`. They should look like

Solutions
```Path≡⊔NoConfusion : (x y : A ⊔ B) → (x ≡ y) ≡ ⊔NoConfusion x y
Path≡⊔NoConfusion = {!!}

isSet⊔NoConfusion : isSet A → isSet B → (x y : A ⊔ B) → isProp (⊔NoConfusion x y)
isSet⊔NoConfusion = {!!}
```

Tip

If you are tired of writing `{A B : Type} →` each time you can stick

```private
variable
A B : Type
```

at the beginning of your `agda` file, and it will assume `A` and `B` implicitly whenever they are mentioned. Make sure it is indented correctly.

Without showing either of these new definitions, try using them to complete `isSet⊔`.

Hint

We can use `pathToFun` or `endPt` to follow how a point of “`isProp` applied to `⊔NoConfusion`” changes into a point of “`isProp` on the path space `x ≡ y`”.

Partial solutions
```isSet⊔ : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔ hA hB x y = pathToFun {!!} (isSet⊔NoConfusion hA hB x y)

isSet⊔' : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔' hA hB x y = endPt {!!} {!!} (isSet⊔NoConfusion hA hB x y)
```

Solutions
```isSet⊔ : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔ hA hB x y = pathToFun (cong isProp (sym (Path≡⊔NoConfusion x y)))
(isSet⊔NoConfusion hA hB x y)

isSet⊔' : {A B : Type} → isSet A → isSet B → isSet (A ⊔ B)
isSet⊔' hA hB x y = endPt (λ A → isProp A) (sym (Path≡⊔NoConfusion x y))
(isSet⊔NoConfusion hA hB x y)
```

### Proving `isSet⊔NoConfusion`

We will now show that `⊔NoConfusion` “is a set”. Locate your definition of `isSet⊔NoConfusion` and try proving it.

Hint

We need to case on the points in `A ⊔ B`.

• If they are both “from `A`” then we need to show that the path spaces in `A` are propositions.

• (2 cases) If they are from different spaces then we must show that the path spaces in `⊥` are propositions.

• If they are both “from `B`” then it is similar to the first case.

## Part 4 - Proving `Path≡⊔NoConfusion`

### It suffices to make an isomorphism

Replicate our proof of `flipPath` in quest 0, it suffices to show an isomorphism instead of an equality. Make this precise in `1FundamentalGroup/Quest2`.

Spoiler

So that you can follow, we will make a lemma (you don’t have to) :

```Path≅⊔NoConfusion : (x y : A ⊔ B) → (x ≡ y) ≅ ⊔NoConfusion x y
Path≅⊔NoConfusion = {!!}
```

To prove the isomorphism (for each arbitrary `x` and `y`) we need four things, which we can extract as local definitions / lemmas using `where`.

Spoiler
```fun : (x y : A ⊔ B) → (x ≡ y) → ⊔NoConfusion x y
fun x y = {!!}

inv : (x y : A ⊔ B) → ⊔NoConfusion x y → x ≡ y
inv x y = {!!}

rightInv : (x y : A ⊔ B) → section (fun x y) (inv x y)
rightInv {A} {B} = {!!}

leftInv : (x y : A ⊔ B) → retract (fun x y) (inv x y)
leftInv = {!!}
```

### `inv`

First try defining `inv : (x y : A ⊔ B) → ⊔NoConfusion x y → x ≡ y`.

Hint 0

Check the goal. You can assume points `x y : A ⊔ B` and a point `h : ⊔NoConfusion x y`. If you case on `x` and `y` you might find there are fewer cases than you need. This is because `⊔NoConfusion (inl ax) (inr by)` was defined to be empty, so `agda` automatically removes the case.

Hint 1

In the case that both points are from `x` we need to show that given a proof `p : ax ≡ ay` we get a proof of `inl ax ≡ inr ay`. We already have the result that if two points are equal then their images under a function are equal.

Solution
```inv : (x y : A ⊔ B) → ⊔NoConfusion x y → x ≡ y
inv (inl x) (inl y) p = cong inl p
inv (inr x) (inr y) p = cong inr p
```

### Attempting `fun`

We try to define the map forward, which we called `fun`. If we assume and case on `x` and `y` in the disjoint sum then

• When `x` and `y` are both from `A` then they will be `inl ax` and `inl ay`, so checking the goal we should be required to give a point in `inl x ≡ inl y → x ≡ y`. Reading this carelessly one could call this “`inl` is injective”.

• When `x` and `y` are from different spaces then checking the goal, we should be required to give a point in `inl ax ≡ inr by → ⊥`. This says there are no paths between the disjoint parts.

• The last case is similar to the first.

We can extract the second case as a lemma :

Spoiler
```disjoint : (a : A) (b : B) → inl a ≡ inr b → ⊥
disjoint a b p = {!!}
```

which we can prove by constructing a subsingleton bundle over `A ⊔ B`, just like we did to prove that `true ≡ false` is empty, in the side quest. In fact this is a generalisation of that result, and the proof also generalises.

Hint

We make a bundle over the disjoint union with the starting fiber as `⊤` and the ending fiber as `⊥`.

Solution
```disjoint : (a : A) (b : B) → inl a ≡ inr b → ⊥
disjoint a b p = endPt bundle p tt where

bundle : A ⊔ B → Type
bundle (inl a) = ⊤
bundle (inr b) = ⊥
```

The other case is quite problematic. This is what we want to show

```inlInj : (x y : A) → (inl {A} {B} x ≡ inl y) → x ≡ y
inlInj x y p = {!!}
```

Here are the problems:

• If we had a map backwards that cancelled `inl` we would be done, but in general this doesn’t exist. For example, if `A` were empty and `B` had a point then we cannot expect to have a map `A ⊔ B → A`.

• There is nothing to induct on : we have no information about `x y : A`. More importantly :

Important

We don’t know how to induct on paths.

Specifically we don’t yet know how to map out of a path space in general.

To find out how to induct on paths, complete quest 4 in trinitarianism, and return to this quest with a completely new perspective.

## Part 5 - Using the Propositional Perspective

After learning about the propositional perspective on equality, we can review some of the things we showed in a new light :

• `a ≡ b → ⊥` can be read as `a` is not equal to `b` since assuming a proof that `a` is equal to `b` we have a point in the empty space.

• In showing an isomorphism between spaces we must show that two functions satisfy `fun (inv x) ≡ x` for each `x` in the domain. This can now be read as `fun` composed with `inv` is equal to the identity on points.

• `isoToPath` says that if two spaces are isomorphic then they are equal.

• `endPt` (`subst` for substitute in the library) takes a bundle and a proof that `x ≡ y` in the base space and substitutes `x` for `y`, hence replacing a point in the fiber of `x` with a point in the fiber of `y`.

• `cong : (f : A → B) → (p : x ≡ y) → f x ≡ f y` says that if two points are equal then their images are equal.

• `true` is not equal to `false`

• `refl` is not equal to `loop`

• `flipPath : Bool ≡ Bool` is a non-trivial equality between `Bool` and itself.

• `inl` is injective (we still have not shown this yet).

• The objective of this whole arc is to show that the fundamental group of the circle is equal to `ℤ`.

• `isProp` says there is at most one point in the space; at most one proof of the proposition. Classically propositions are meant to only have a single proof (“proof irrelevance”), because for propositions `A` and `B`, having implications `A → B` and `B → A` is enough to show `A ≡ B`.

• `isSet` says between any two points there is at most one path between them, i.e. “there is only `refl`”, i.e. the space is disjoint.

We shall apply this perspective to the problem at hand.

### `fun`

Now that we know how to induct on paths, we need to pick a path to induct on. Continuing with trying to show that `inl` is injective we will notice that path induction does not actually work here, since we have

• a start point `ax : A`

• a variable end point `ay : A`

• but the path is in the disjoint union `inl ax ≡ inl ay` not a path in `A`

We instead take a step back and look at `fun` itself. (You can now abandon `inlInj` if you like, this will become a corollary of the classification.) We also remove the cases so that we are back to just having

```fun : (x y : A ⊔ B) → (x ≡ y) → ⊔NoConfusion x y
fun x y = {!!}
```

You might have noticed by now that we are in the perfect position to induct on paths in `x ≡ y`. Path induction - `J` - says that to make a function `(x y : A ⊔ B) → (x ≡ y) → ⊔NoConfusion x y`, it suffices just to give a point in `⊔NoConfusion x x`. Formalise the above (without showing `⊔NoConfusion x x` yet) :

Spoiler
```fun : (x y : A ⊔ B) → (x ≡ y) → ⊔NoConfusion x y
fun x y = J (λ y' p → ⊔NoConfusion x y') {!!}
```

To prove `⊔NoConfusion x x` it would be convenient to be able to case on `x` so we will extract it as a lemma. Once you extract and case on `x` this it should be quite easy to show.

Spoiler
```⊔NoConfusionSelf : (x : A ⊔ B) → ⊔NoConfusion x x
⊔NoConfusionSelf (inl x) = refl
⊔NoConfusionSelf (inr x) = refl
```

### `rightInv`

Try to define `rightInv : (x y : A ⊔ B) → section (fun x y) (inv x y)`.

Hint 0

It is a good idea to case on `x` and `y` in the space `A ⊔ B`, since `inv` is the first to take these inputs in here, and `inv` was defined by casing on `x` and `y`. This should reduce us to just two cases, like when defining `inv`. We will just describe the case when they are both from `A`.

Hint 1

We can use `J` to reduce to the case of when the path is `refl`. (No proof of the `refl` case yet.)

Solution
```rightInv : (x y : A ⊔ B) → section (fun x y) (inv x y)
rightInv {A} {B} (inl x) (inl y) p =
J (λ y' p → fun {A} {B} (inl x) (inl y') (inv (inl x) (inl y') p) ≡ p) {!!}
```

We added the implicit arguments `{A}` and `{B}` so we can actually access them here. The remaining hole is for showing that

```fun (inl x) (inl x) (inv (inl x) (inl x) refl) ≡ refl
```

Hint 2

It would help to make a chain of equalities. We defined `inv (inl x) (inl x) refl` to be `refl`, so we only need to show that

```fun (inl x) (inl x) refl ≡ refl
```

Since `fun` was defined using `J` we need to know how `J` computes when it is fed `refl`. We described this before, it is called `JRefl`.

Solution
```rightInv : (x y : A ⊔ B) → section (fun x y) (inv x y)
rightInv {A} {B} (inl x) (inl y) p = J (λ y' p → fun {A} {B} (inl x) (inl y') (inv (inl x) (inl y') p) ≡ p)
(
fun {A} {B} (inl x) (inl x) refl
≡⟨ JRefl {x = inl x} ((λ y' p → ⊔NoConfusion {A} {B} (inl x) y')) _ ⟩
-- uses how J computes on refl
refl ∎
) p
rightInv {A} {B} (inr x) (inr y) p = {!!}
```

### `leftInv`

Try to define `leftInv`.

Hint 0

We do this but each part of this proof will be relevant anywayuse `J` since `fun` “happens first”. This should reduce the problem to showing

```inv x x (fun x x refl) ≡ refl
```

Solution
```leftInv : (x y : A ⊔ B) → retract (fun x y) (inv x y)
leftInv x y = J (λ y' p → inv x y' (fun x y' p) ≡ p) {!!}
```

Hint 1

If you extract what is needed as a lemma you can case on the variable. Remember to use `JRefl` for the application of `fun`.

Solution
```leftInv : (x y : A ⊔ B) → retract (fun x y) (inv x y)
leftInv x y = J (λ y' p → inv x y' (fun x y' p) ≡ p)
(
(inv x x (fun x x refl))
≡⟨ cong (inv x x) (JRefl ((λ y' p → ⊔NoConfusion x y')) _) ⟩
inv x x (⊔NoConfusionSelf x)
≡⟨ lem x ⟩
refl ∎
) where

lem : (x : A ⊔ B) → inv x x (⊔NoConfusionSelf x) ≡ refl
lem (inl x) = refl
lem (inr x) = refl
```