# 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 spacethere is a path

`p : A ≡ ⊥`

in the space of spaces`Type`

from`A`

to the empty spacethere 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