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