Quest 3  The Loop Space is ℤ
In Quest 1  Loop Space of the Circle we introduced our main
method of proving that the fundamental group
(which we take to be loopSpace S¹ base
for now)
is ℤ
,
and in Quest 2  ℤ is a Set we decided that this
means to show that they are equal spaces.
.. admonition:: The Goal
loopSpace≡ℤ : loopSpace S¹ base ≡ ℤ loopSpace≡Z = {!!}
As usual we will show this via giving an isomorphism,
so we must make comparison maps forward and back.
However, we discovered we had to define the backwards map
over all of S¹
.
We already have windingNumber
, the forwards comparison map,
which gives us a map loopSpace S¹ base → ℤ
when applied to base
.
windingNumber : (x : S¹) → base ≡ x → helix x
In this quest our goal is to make a map backwards
Current Goal
rewind : (x : S¹) → helix x → base ≡ x
Since windingNumber
took a path and found how
many times the path loops around, in general “an integer twisted around the helix a bit”,
or “an integer plus a bit”.
We want to make rewind
do the reverse.
So rewind
should take “an integer n
plus a bit”,
loop around n
times, then add that extra corresponding bit,
the path from base
to x
to the end.
Part 0  rewind
Dependent paths
We try making rewind
.
We can assume a point x : S¹
,
then case on what it is.
rewind : (x : S¹) → helix x → base ≡ x
rewind base = {!!}
rewind (loop i) = {!!}
In the case of base
we want a map
from helix base
i.e. ℤ
, to base ≡ base
.
Try filling this in.
Solution
We want this to be the correct inverse,
described as looping around n
times and adding that extra bit on the end.
However there is nothing to add at the end in this case,
so it should just be loop_times
,
which we already defined in Quest 1  Loop Space of the Circle.
The case of loop i
will be a lot more work.
Checking the goal we see that at each point loop i
on the loop, it wants a point in the space
helix (loop i) → base ≡ (loop i)
,
which it might reduce to sucℤPath i → base ≡ (loop i)
according to the definition of helix
.
Collecting these spaces together along this i
,
we obtain a loop in the space of spaces based at the space ℤ → base ≡ base
given by
λ i → helix (loop i) → base ≡ (loop i) : (ℤ → base ≡ base) ≡ (ℤ → base ≡ base).
Now collecting the points we need to give into a “path” as well,
we obtain the notion of a dependent path :
each point of this “path” belongs to a space along the path of spaces.
We define dependent paths and design a way of mapping out of
S¹
in general in Quest 5  Dependent Paths from Trinitarianism.
We assume from now on knowledge of dependent paths.
Using outOfS¹
Now that we have a way of mapping out of S¹
(using PathD
),
called outOfS¹D
,
try to use it to repackage the work we have to far.
Solution
Originally we have
rewind : (x : S¹) → helix x → base ≡ x
rewind base = loop_times
rewind (loop i) = {!!}
Now we rearrange this to
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times {!!}
since our bundle over S¹
is (λ x → helix x → base ≡ x)
and our image for base
is loop_times
.
Checking the last goal, it remains to give a dependent path of type
PathD (λ i → sucℤPath i → base ≡ loop i) loop_times loop_times
.
Remembering the definition of PathD
,
this should be exactly giving a path
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times ≡ loop_times
,
since PathD
reduces the issue of dependent paths to just paths in
the end space, which is ℤ → base ≡ base
in this case.
Let’s make this a chain of equalities :
Solution
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ {!!} ⟩
loop_times ∎
)
Functions and pathToFun
The map loop_times
takes an integer and
does loop
that many times.
On the other hand pathToFun
follows how loop_times
changed along the path of spaces λ i → sucℤPath i → base ≡ loop i
,
and spits out the corresponding point at the end.
This path of spaces is specifically a path of function spaces,
so we need to find a more explicit way of describing what pathToFun
does to spaces of functions.
To generalize, suppose we have spaces A0 A1 B0 B1 : Type
and paths A : A0 ≡ A1
and B : B0 ≡ B1
.
Then let pAB
denote the path
λ i → A i → B i : (A0 → B0) ≡ (A1 → B1)
.
We want to figure out what pathToFun
does when it follows a function f : A0 → B0
along the path pAB
.
We know by functional extensionality that the function
pathToFun pAB f : A1 → B1
should be determined by what it does to terms in A1
,
so we can assume a1 : A1
.
The idea is we “apply f
by sending a1
back to A0
”.
Since pathToFun (sym A) a1
is meant to give the point in A0
that “looks like a1
”, we try applying f
to this point,
then send it across again via the path B
to the point
f (pathToFun (sym A) a1)
looks like in B1
.
We expect the outcome to be the same.
pathToFun→ : {A0 A1 B0 B1 : Type} {A : A0 ≡ A1} {B : B0 ≡ B1} (f : A0 → B0) →
pathToFun (λ i → A i → B i) f ≡ λ a1 → pathToFun B (f (pathToFun (sym A) a1))
The proof of this in cubical agda
is simply refl
,
so we need not even extract it as a lemma.
A cubical hack
Is actually one of the axioms asserted in cubical agda
that pathToFun (λ i → A i → B i) f
is externally equal to
λ a1 → pathToFun B (f (pathToFun (sym A) a1))
.
Here we are using the cubical
definition of pathToFun
so we can simply give refl
for its proof.
However, according the definition of pathToFun
we gave
in Trinitarianism, they are not externally equal
but can be shown to be internally equal using J
.
We prove this from our own definitions
here.
We interpret what this result means in our specific case :
We are making pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
into another map in the space ℤ → base ≡ base
,
by following along the diagram
Specifically, this map should take n : ℤ
and first send it backwards along
sucℤPath
, supposedly giving us n  1
.
Then it applies loop_times
, obtaining the loop loop (n  1) times
.
Lastly it follows loop (n  1) times
along the path λ i → base ≡ loop i
(which itself is a loop starting and ending at base ≡ base
in the space of spaces),
obtaining some path from base ≡ base
, which we expect to be internally
equal to loop n times
.
Try putting this together in our definition of rewind
,
as a new intermediate step in our chain of equalities.
Solution
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ {!!} ⟩
loop_times ∎
)
We can simplify the above expression.
We know that pathToFun (sym sucℤPath) n
should follow n
along sucℤPath
backwards, so it should be n  1
.
We can use this to move a step closer to the goal.
Solution
This equality is definitional.
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ refl ⟩
(λ n → pathToFun (λ i → base ≡ loop i) (loop (predℤ n) times))
≡⟨ {!!} ⟩
loop_times ∎
)
The path fibration and pathToFun
It remains to find out how pathToFun
interacts with the path of loops coming out of base.
We call “the path of loops coming out of base” λ i → base ≡ loop i
the path fibration
at base
.
The animation tells us that we are gradually concatenating the input loop (n  1) times
with loop
.
Hence we should obtain loop (n  1) times ∙ loop
.
We are a bit lucky here, and these are in fact definitionally equal,
but to justify this in general, we can prove that
“following along the path fibration is the same as concatenating”.
pathToFunPathFibration : {A : Type} {x y z : A} (q : x ≡ y) (p : y ≡ z) →
pathToFun (λ i → x ≡ p i) q ≡ q ∙ p
This is in fact a quick exercise.
Hint
We take the propositional perspective 
without loss of generality we can assume
y
and z
are exactly the same.
Crucially : we know what pathToFun
does to refl
(recall pathToFunRefl
from the quest on paths).
Solution
pathToFunPathFibration : {A : Type} {x y z : A} (q : x ≡ y) (p : y ≡ z) →
pathToFun (λ i → x ≡ p i) q ≡ q ∙ p
pathToFunPathFibration {A} {x} {y} q = J (λ z p → pathToFun (λ i → x ≡ p i) q ≡ q ∙ p)
(
pathToFun refl q
≡⟨ pathToFunRefl q ⟩
q
≡⟨ ∙Refl q ⟩
q ∙ refl ∎
)
To include this in rewind
we have
Spoiler
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩  how pathToFun interacts with →
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ refl ⟩  sucℤPath is just taking successor, and so its inverse is definitionally taking predecessor
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (predℤ n)))
≡⟨ funExt (λ n → pathToFunPathFibration _ _) ⟩  how pathToFun interacts with the "path fibration"
(λ n → (loop (predℤ n) times) ∙ loop)
≡⟨ {!!} ⟩
loop_times ∎
)
There are several ways to complete this final part. We will leave the rest in a hint.
Hint
Applying functional extensionality we just need to show that for each n : ℤ
the outputs are equal, i.e. loop predℤ n times ∙ loop ≡ loop n times
.
By our design of loop_times
we should have that
loop m times ∙ loop
is equal to loop (m + 1) times
.
Then we are reduced to showing that loop (sucℤ predℤ n) times ≡ loop n times
,
or just sucℤ predℤ n ≡ n
.
Solution
rewind : (x : S¹) → helix x → base ≡ x
rewind = outOfS¹D (λ x → helix x → base ≡ x) loop_times
(
pathToFun (λ i → sucℤPath i → base ≡ loop i) loop_times
≡⟨ refl ⟩  how pathToFun interacts with →
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (pathToFun (sym sucℤPath) n)))
≡⟨ refl ⟩  sucℤPath is just taking successor, and so its inverse is definitionally taking predecessor
(λ n → pathToFun (λ i → base ≡ loop i) (loop_times (predℤ n)))
≡⟨ funExt (λ n → pathToFunPathFibration _ _) ⟩  how pathToFun interacts with the "path fibration"
(λ n → (loop (predℤ n) times) ∙ loop)
≡⟨ funExt (λ n →
loop predℤ n times ∙ loop
≡⟨ loopSucℤtimes (predℤ n) ⟩
loop (sucℤ (predℤ n)) times
≡⟨ cong loop_times (sucℤPredℤ n) ⟩
loop n times ∎) ⟩
loop_times ∎
)
We can check that rewind base
is indeed loop_times
by using Cc Cn
.
This is to be expected as outOfS¹
evaluated at base
should back exactly what we fed it,
as mentioned in the discussion on mapping out of the circle.
Part 1  rewind
is a right inverse
We are now in a position to approach the main goal :
loopSpaceS¹≡ℤ : loopSpace S¹ base ≡ ℤ
loopSpaceS¹≡ℤ = {!!}
We have reduced this to giving an isomorphism,
which involves giving the map windingNumber base
forward
and loop_times
backwards,
and showing that they are inverses of each other.
Hence the next step is to show that
“looping n
times then taking the winding number gives back n
”.
Try to state and prove this in 1FundamentalGroup/Quest3.agda
.
In the hints we will use intuitive notation for integers
that may not align exactly with agda
code.
The statement
windingNumberRewindBase : (n : ℤ) → windingNumber base (rewind base n) ≡ n
windingNumberRewindBase = {!!}
We identify rewind base
with loop_times
,
since they are externally equal.
Hint 0
Since loop_times
was defined by casing on n
we case on n

it could be zero, a positive integer, negative one, or less than negative one.
Hint 1
Some of the cases are trivial 
we know exactly what loop 0 times
and windingNumber base loop
are.
Solution for Hint 1
windingNumberRewindBase : (n : ℤ) → windingNumber base (rewind base n) ≡ n
windingNumberRewindBase (pos zero) = refl
windingNumberRewindBase (pos (suc n)) = {!!}
windingNumberRewindBase (negsuc zero) = refl
windingNumberRewindBase (negsuc (suc n)) = {!!}
Hint 2
We can identify windingNumber base
with its definition,
reducing the problem to showing that
endPt helix (loop n times) 0
is equal to n
,
in the separate cases.
For the first case,
we can reduce loop (n + 1) times
to just loop n times ∙ loop
since that was the definition.
Hence we are interested in what endPt helix (loop n times ∙ loop) 0
is.
Recalling our intuition behind endPt
,
this amounts to following the point 0
up the helix
along the path
loop n times ∙ loop
.
This should just be going to endPt helix (loop n times) 0
then adding 1
.
You can also check what agda
reduces the expression to by writing it in the hole and
then doing Cc Cn
.
It should look something like sucℤ (transp (λ i → helix (loop pos n times i)) i0 (pos 0))
.
Clearly it has reduced the definition a bit too far,
but the important idea is there, that it is + 1
of whatever data we have already.
Lastly we can just take sucℤ
on both sides of an equality we have from the induction hypothesis.
Solution
For one of the cases we detail the thought process going on above, and for the last case we extract only the important part of the proof.
windingNumberRewindBase : (n : ℤ) → windingNumber base (rewind base n) ≡ n
windingNumberRewindBase (pos zero) = refl
windingNumberRewindBase (pos (suc n)) =
windingNumber base (rewind base (pos (suc n)))
≡⟨ refl ⟩
windingNumber base (loop (pos n) times ∙ loop)
≡⟨ refl ⟩
endPt helix (loop (pos n) times ∙ loop) (pos zero)
≡⟨ refl ⟩
sucℤ (endPt helix (loop (pos n) times) (pos zero))
≡⟨ cong sucℤ (windingNumberRewindBase (pos n)) ⟩
sucℤ (pos n)
≡⟨ refl ⟩
pos (suc n) ∎
windingNumberRewindBase (negsuc zero) = refl
windingNumberRewindBase (negsuc (suc n)) = cong predℤ (windingNumberRewindBase (negsuc n))
You might wonder if it is possible to make the above map work across all of S¹
,
and the answer is yes.
This is not really necessary for our goal,
so feel free to skip to the next part if you are not interested.
Try stating and proving the generalization of the above;
which we call windingNumberRewind
.
The Statement
windingNumberRewind : (x : S¹) (n : helix x) → windingNumber x (rewind x n) ≡ n
windingNumberRewind = {!!}
Hint 0
We defined rewind
by casing on points in the circle
and rewind
is the first function being applied,
so it would make sense to case on points in the circle.
In the case when the point is base
we can just give
the map we wanted to generalize in the first place.
Solution to Hint 0
windingNumberRewind : (x : S¹) (n : helix x) → windingNumber x (rewind x n) ≡ n
windingNumberRewind =
outOfS¹D (λ x → (n : helix x) → windingNumber x (rewind x n) ≡ n)
windingNumberRewindBase {!!}
Hint 1
Checking the last hole we see that we need to give a dependent path from
windingNumberRewindBase
to itself.
According to the definition of a dependent path,
this is just a path in the last fiber from pathToFun
of windingNumberRewindBase
to windingNumberRewindBase
(the fiber is (n : ℤ) → windingNumber base (rewind base n) ≡ n
).
Now this might seem very complicated :
even after applying functional extensionality (this is equality of two functions)
this would be “finding a path between paths in ℤ
”.
Try repeating that last bit in your head a couple of times.
Hint 2
We put a lot of effort into showing that ℤ
is a set.
Solution
windingNumberRewind : (x : S¹) (n : helix x) → windingNumber x (rewind x n) ≡ n
windingNumberRewind =  must case on x / use recursor / outOfS¹ since that is def of rewind
outOfS¹D (λ x → (n : helix x) → windingNumber x (rewind x n) ≡ n)
windingNumberRewindBase (
pathToFun
(λ i → (n : helix (loop i)) → windingNumber (loop i) (rewind (loop i) n) ≡ n)
windingNumberRewindBase
≡⟨ funExt (λ x → isSetℤ _ _ _ _ ) ⟩
windingNumberRewindBase ∎)
Part 2  rewind
is a left inverse
Try to show that rewind
is a left inverse.
The Statement
Just like we struggled to only define windingNumber base
without access to the entire circle,
we make sure to include all the data we have access to.
Note that this was not the case before.
rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = {!!}
Hint 0
Remembering that windingNumber x p
is externally equal to endPt helix p 0
,
and that endPt
is defined by path induction  using J
(this is not exactly true for endPt
from the library for cubical
reasons),
the obvious thing to do here is to do path induction.
Solution for Hint 0
rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p) {!!}
Hint 1
It suffices to show that rewind x (windingNumber x refl) ≡ refl
,
which by reducing the left side is the same as showing
loop_times (endPt helix refl 0) ≡ refl
.
Solution to Hint 1
rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p)
(rewind base (windingNumber base refl)
≡⟨ refl ⟩
loop_times (endPt helix (refl {x = base}) (pos zero))
≡⟨ {!!} ⟩
refl ∎)
Hint 2
We know what endPt
does to refl
, which is given by the result endPtRefl
.
If you need to recall what endPtRefl
proves you can type it into the hole
and do Cc C.
for the goal and the type of endPtRefl
.
Solution to Hint 2
rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p)
(rewind base (windingNumber base refl)
≡⟨ refl ⟩
loop_times (endPt helix (refl {x = base}) (pos zero))
≡⟨ cong loop_times (cong (λ g → g (pos zero)) (endPtRefl {x = base} helix)) ⟩
loop (pos zero) times
≡⟨ {!!} ⟩
refl ∎)
Solution
The last step is simply remembering how loop_times
computes.
rewindWindingNumber : (x : S¹) (p : base ≡ x) → rewind x (windingNumber x p) ≡ p
rewindWindingNumber x = J (λ x p → rewind x (windingNumber x p) ≡ p)
(rewind base (windingNumber base refl)
≡⟨ refl ⟩
loop_times (endPt helix (refl {x = base}) (pos zero))  reduce both definitions
≡⟨ cong loop_times (cong (λ g → g (pos zero)) (endPtRefl {x = base} helix)) ⟩
loop (pos zero) times
≡⟨ refl ⟩
refl ∎)
Part 3  The Loop Space is ℤ
We can conclude our main goal now, by collecting all of the components we have made above. We leave you the pleasure.
Solution
As usual we construct an isomorphism,
but we can choose to do this over the entire circle
or just between loopSpace S¹ base
and ℤ
.
We do the former and have the latter as a corollary,
but you could just do the latter directly as well.
pathFibration≡helix : (x : S¹) → (base ≡ x) ≡ helix x
pathFibration≡helix x =
isoToPath (iso (windingNumber x) (rewind x) (windingNumberRewind x) (rewindWindingNumber x))
loopSpaceS¹≡ℤ : loopSpace S¹ base ≡ ℤ
loopSpaceS¹≡ℤ = pathFibration≡helix base
What now?
We have mentioned already that we aren’t exactly working with the fundamental group, but the loop space. In the final quest of this arc we discuss the definition of the fundamental group and show that the loop space in this case is the fundamental group already.