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