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