# Quest 0 - Side Quests

## Different notions of “empty”

The following are “the same”,

• 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 ≅ ⊥` (input `\cong` for `≅`) of spaces

Here we will take “the same” to mean there are maps from any one to another (they are “propositionally the same”). We will first define the three.

In `1FundamentalGroup/Quest0.agda`, uncomment this side quest and locate these three definitions :

```_toEmpty : (A : Type) → Type
A toEmpty = {!!}

pathEmpty : (A : Type) → Type₁
pathEmpty A = {!!}

isoEmpty : (A : Type) → Type
isoEmpty A = {!!}
```

Note

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

Tip

`agda` supports unicode symbols such as `⊥`. See here for how to insert `⊥` and other symbols.

Try to fill them in according to the above. You may have noticed we used `Type₁` in the second definition. To find out what `Type₁` is, see Part 3 - Universes in Trinitarianism.

Check that your definitions are the same as ours by comparing with the solutions in `1FundamentalGroup/Quest0Solutions.agda`. We will make maps from `toEmpty A` to `isoEmpty A` to `pathEmpty A` and back to `toEmpty A`.

First we show that the empty space maps into any other space. This is very useful when working with the empty space.

```outOf⊥ : (A : Type) → ⊥ → A
outOf⊥ = {!!}
```

Try to fill in the definition without looking at the hint.

Hint

Recall the definition of the empty space being a CW-complex with nothing in it. We can always case on variable points from CW-complexes. What cases are there?

We fill in `toEmpty→isoEmpty`

```toEmpty→isoEmpty : (A : Type) → toEmpty A → isoEmpty A
toEmpty→isoEmpty A = {!!}
```

Tip

You can use `where` to extract lemmas / make local definitions like we did in defining `flipIso`; see here.

Hint 0
• Check the goal to see what we have and what we need to give.

• Assume `f : toEmpty A` by putting an `f` before the `=`.

• Refine the goal to see what `agda` suggests.

Hint 1
• We need to give an isomorphism, i.e. a map from `A` to `⊥`, and a map from `⊥` to `A`, and proofs that these satisfy `section` and `retract` respectively.

• If we have a point in `⊥` then we can get a point in any space.

Try filling in

```isoEmpty→pathEmpty : (A : Type) → isoEmpty A → pathEmpty A
isoEmpty→pathEmpty A = {!!}
```

Hint

We converted an isomorphism to a path in quest 0.

Lastly try filling in

```pathEmpty→toEmpty : (A : Type) → pathEmpty A → toEmpty A
pathEmpty→toEmpty A = {!!}
```
• Check the goal

• We can assume a path `p : pathEmpty A`

• Check the goal again

• Since `toEmpty A` as defined as `A → ⊥` we can assume a point `x : A`

• We can follow the point `x` along the path `p` using `pathToFun`, as we did for `flipPath` in Quest 0 - Working with the Circle.

## Proving `true≢false`

Locate `1FundamentalGroup/Quest0SideQuests/TrueNotFalse.agda` we will show

```true≢false : true ≡ false → ⊥
true≢false = {!!}
```

We do this by making a subsingleton bundle over `Bool` whose fiber over `true` is the singleton space `⊤` and fiber over `false` is the empty space `⊥`. The definition of `⊤` is

```data ⊤ : Type where
tt : ⊤
```
• Assume a path `h : true ≡ false`

• Define a map from `Bool` to `Type` (as a lemma or using where), that takes `true` to `⊤` and `false` to `⊥`. This is a subsingleton bundle over `Bool`, since each fiber is `⊤` and `⊥`, having only a single or no points.

• We can follow how the point `tt : ⊤` changes along the path `h` using `pathToFun`, as we did for `flipPath` in Quest 0 - Working with the Circle. This should give you a point in the empty space `⊥`.

Due to the previous side quest Different notions of “empty” this tells us that the space `true ≡ false` is empty.

## Defining `cong`

Under construction