md files removed and readme.rst added
This commit is contained in:
Jlh18
parent
b32ce74c65
commit
31d9f67af6
@ -1,118 +0,0 @@
|
||||
The Circle
|
||||
=======================
|
||||
|
||||
In this series of quests we will prove that the fundamental group
|
||||
of `S¹` is `ℤ`.
|
||||
In fact, our strategy will also show that the higher homotopy groups of
|
||||
`S¹` are all trivial.
|
||||
We begin by formalising the problem statement.
|
||||
|
||||
A contruction of 'the circle' is :
|
||||
|
||||
- a point called `base`
|
||||
- an edge from that point to itself called `loop`
|
||||
|
||||
Here is our definition of the circle in `agda`.
|
||||
|
||||
```agda
|
||||
data S¹ : Type where
|
||||
base : S¹
|
||||
loop : base ≡ base
|
||||
```
|
||||
|
||||
The `base ≡ base` is the _space of paths from `base` to `base`_.
|
||||
The definition asserts that there is a point called `loop`
|
||||
in `base ≡ base`, i.e. a path from `base` to itself.
|
||||
Whenever we have a colon like `S¹ : Type` or `base : S¹`
|
||||
it says the former is a point in the latter,
|
||||
where the latter is viewed as a space;
|
||||
in the first case `Type` is the space of spaces.
|
||||
|
||||
<p>
|
||||
<details>
|
||||
<summary>Further details</summary>
|
||||
|
||||
This is called a _higher inductive type_ (HIT), which generally
|
||||
follows the format of
|
||||
|
||||
- `data`
|
||||
- the name of the HIT - in our case `S¹`
|
||||
- the _type_ of the HIT, in our case `Type`
|
||||
- `where` followed by
|
||||
- the _constructors_ of the HIT, in our case `base` and `loop`,
|
||||
which we will think of as vertices, edges, surfaces, and so on
|
||||
|
||||
</details>
|
||||
</p>
|
||||
|
||||
An "edge" is the same as a path.
|
||||
There are other paths in `S¹`,
|
||||
for example the _constant path at `base`_.
|
||||
In `1FundamentalGroup/Quest0.agda` naviage to
|
||||
|
||||
```agda
|
||||
Refl : base ≡ base
|
||||
Refl = {!!}
|
||||
```
|
||||
|
||||
we will guide you through defining it.
|
||||
We are about to construct a path `Refl : base ≡ base`
|
||||
(read path `Refl` from `base` to `base`)
|
||||
The _hole_ `{ }0` is where you describe the path.
|
||||
We will fill the hole `{ }0`.
|
||||
|
||||
- enter `C-c C-l` (this means `Ctrl-c Ctrl-l`).
|
||||
Whenever you do this, `agda` will check the document is written correctly.
|
||||
This will open the `*Agda Information*` window looking like
|
||||
|
||||
```
|
||||
?0 : base ≡ base
|
||||
?1 : (something)
|
||||
?2 : (something)
|
||||
...
|
||||
```
|
||||
|
||||
This says you have some unfilled _holes_.
|
||||
- navigate to the hole `{ }0` using `C-c C-f` (forward) or `C-c C-b` (backward)
|
||||
- enter `C-c C-r`. The `r` stands for _refine_.
|
||||
Whenever you do this whilst having your cursor in a hole,
|
||||
Agda will try to help you.
|
||||
- you should now see `λ i → { }1`.
|
||||
This is `agda` suggesting that for each
|
||||
`i : I` (if you like you can think of this as a generic point
|
||||
on the the unit interval `I`)
|
||||
you give a point in between the start and end of the path.
|
||||
This is all you need to specify a path in `agda`.
|
||||
- navigate to that new hole
|
||||
- enter `C-c C-,` (this means `Ctrl-c Ctrl-comma`).
|
||||
Whenever you make this command whilst having your cursor in a hole,
|
||||
`agda` will check the _goal_, i.e. what kind of thing you need to stick in.
|
||||
- the goal (`*Agda information*` window) should look like
|
||||
|
||||
```
|
||||
Goal: S¹
|
||||
—————————————————————————
|
||||
i : I
|
||||
———— Constraints ——————————————
|
||||
...
|
||||
```
|
||||
you see that `agda` knows you have a generic point
|
||||
`i : I` on the unit interval.
|
||||
All the constraints are saying that when you look
|
||||
at `i = 0` and `i = 1`, whatever you give in between must
|
||||
match up with the end points of the path,
|
||||
namely `base` and `base`
|
||||
- write `base` in the hole, since this is the constant path
|
||||
- press `C-c C-SPC` to fill the hole with `base`.
|
||||
In general when you have some text (and your cursor) in a hole,
|
||||
doing `C-c C-SPC` will tell `agda` to replace the hole with that text.
|
||||
`agda` will give you an error if it can't make sense of your text.
|
||||
- the number of holes in the `*Agda Information*`
|
||||
window should have gone down by one,
|
||||
this means `agda` has accepted what you filled this hole with.
|
||||
Just to be sure you can also reload the `agda` file and check
|
||||
that `agda` has no complaints.
|
||||
- if you want to play around with this you can start again
|
||||
by replacing what you wrote with `?` and doing
|
||||
`C-c C-l`
|
||||
|
||||
@ -1,104 +0,0 @@
|
||||
# `Refl ≡ loop` is empty
|
||||
|
||||
To get a better feel of `S¹`, we show that the space of paths (homotopies) between
|
||||
`Refl` and `loop`, written `Refl ≡ loop`, is empty.
|
||||
First, we define the empty space and what it means for a space to be empty.
|
||||
Here is what this looks like in `agda` :
|
||||
|
||||
```agda
|
||||
data ⊥ : Type where
|
||||
```
|
||||
|
||||
This says "the empty space `⊥` is a space with no points in it".
|
||||
|
||||
Here are three candidate definitions for a space `A` to be empty :
|
||||
|
||||
- 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 ≅ ⊥` of spaces
|
||||
|
||||
These turn out to be 'the same' (see `1FundamentalGroup/Quest0SideQuests/SideQuest0`),
|
||||
however for our present purposes we will use the first definition.
|
||||
Our goal is therefore to produce a point in the function space
|
||||
|
||||
```agda
|
||||
( Refl ≡ loop ) → ⊥
|
||||
```
|
||||
|
||||
The authors of this series have thought long and hard
|
||||
about how one would come up with the following argument.
|
||||
Unfortunately, sometimes mathematics is in need of a new trick
|
||||
and this was one of them.
|
||||
|
||||
> The trick is to make a path `p : true ≡ false` from the assumed path (homotopy) `h : Refl ≡ loop` by
|
||||
> constructing a non-trivial `Bool`-bundle over the circle,
|
||||
> hence obtaining a map `( Refl ≡ loop ) → ⊥`.
|
||||
|
||||
To elaborate :
|
||||
`Bool` here refers to the discrete space with two points `true, false`.
|
||||
(To find out the definition of `Bool` in `agda`
|
||||
you can hover over `Bool` in `agda` and use `M-SPC c d`.)
|
||||
We will create a map `doubleCover : S¹ → Type` that sends
|
||||
`base` to `Bool` and the path `loop` to a non-trivial path `flipPath : Bool ≡ Bool`
|
||||
in the space of spaces.
|
||||
|
||||
<img src="images/doubleCover.png"
|
||||
alt="doubleCover"
|
||||
width="1000"
|
||||
class="center"/>
|
||||
|
||||
Viewing the picture vertically,
|
||||
for each point `x : S¹`,
|
||||
we call `doubleCover x` the _fiber of `doubleCover` over `x`_.
|
||||
All the fibers look like `Bool`, hence our choice of the name _`Bool`-bundle_.
|
||||
|
||||
We will get a path from `true` to `false`
|
||||
in the fiber of `doubleCover` over `base`
|
||||
by 'lifting the homotopy' `h : Refl ≡ loop` and considering the end points of
|
||||
the 'lifted paths'.
|
||||
`Refl` will 'lift' to a 'constant path' and `loop` will 'lift' to
|
||||
|
||||
<img src="images/lifted_loops.png"
|
||||
alt="lifted_loops"
|
||||
width="1000"
|
||||
class="center"/>
|
||||
|
||||
Let's assume for the moment that we have `flipPath` already and
|
||||
define `doubleCover`.
|
||||
|
||||
- Navigate to the definition of `doubleCover` and make sure
|
||||
you have loaded the file with `C-c C-l`.
|
||||
```agda
|
||||
doubleCover : S¹ → Type
|
||||
doubleCover x = {!!}
|
||||
```
|
||||
- Navigate your cursor to the hole,
|
||||
write `x` and do `C-c C-c`.
|
||||
The `c` stands for _cases_.
|
||||
You should now see two new holes :
|
||||
|
||||
```agda
|
||||
doubleCover : S¹ → Type
|
||||
doubleCover base = {!!}
|
||||
doubleCover (loop i) = {!!}
|
||||
```
|
||||
|
||||
This means :
|
||||
`S¹` is made from a point `base` and an edge `loop`,
|
||||
so a map out of `S¹` to a space is the same as choosing
|
||||
a point and an edge to map `base` and `loop` to respectively.
|
||||
Since `loop` is a path from `base` to itself,
|
||||
its image must also be a path from the image of `base` to itself.
|
||||
- Use `C-c C-f` and/or `C-c C-b` to navigate to the first hole.
|
||||
We want to map `base` to `Bool` so
|
||||
fill the hole with `Bool` using `C-c C-SPC`.
|
||||
- Navigate to the second hole.
|
||||
Here `loop i` is a generic point in the path `loop`,
|
||||
where `i : I` is a generic point of the 'unit interval'.
|
||||
We want to map `loop` to `flipPath`,
|
||||
so `loop i` should map to a generic point in the path `flipPath`.
|
||||
Try filling the hole.
|
||||
- Once you think you are done, reload the `agda` file with `C-c C-l`
|
||||
and if it doesn't complain this means there are no problems with your definition.
|
||||
|
||||
Defining `flipPath` is quite involved and we will do so in the next quest!
|
||||
@ -1,187 +0,0 @@
|
||||
# `Refl ≡ loop` is empty - Defining `flipPath` via Univalence
|
||||
|
||||
In this part, we will define the path `flipPath : Bool ≡ Bool`.
|
||||
Recall the picture of `doubleCover`.
|
||||
|
||||
<img src="images/doubleCover.png"
|
||||
alt="doubleCover"
|
||||
width="1000"
|
||||
class="center"/>
|
||||
|
||||
This means we need `flipPath` to correspond to
|
||||
the unique non-identity permutation of `Bool`
|
||||
that flips `true` and `false`.
|
||||
|
||||
We proceed in steps :
|
||||
|
||||
1. Define the function `Flip : Bool → Bool`.
|
||||
2. Promote this to an isomorphism `flipIso : Bool ≅ Bool`.
|
||||
3. We use _univalence_ to turn `flipIso` into
|
||||
a path `flipPath : Bool ≡ Bool`.
|
||||
The univalence axiom asserts that
|
||||
paths in `Type` - the space of spaces - correspond to
|
||||
homotopy-equivalences of spaces.
|
||||
As a corollary,
|
||||
we can make paths in `Type` from isomorphisms in `Type`.
|
||||
|
||||
## The function
|
||||
|
||||
- In `1FundamentalGroup/Quest0.agda`, navigate to :
|
||||
|
||||
```agda
|
||||
Flip : Bool → Bool
|
||||
Flip x = {!!}
|
||||
```
|
||||
- Write `x` inside the hole,
|
||||
and do `C-c C-c` with your cursor still inside.
|
||||
You should now see :
|
||||
```agda
|
||||
Flip : Bool → Bool
|
||||
Flip false = {!!}
|
||||
Flip true = {!!}
|
||||
```
|
||||
This means :
|
||||
the space `Bool` is made of two points `false, true` and nothing else,
|
||||
so to map out of `Bool` it suffices
|
||||
to find images for `false` and `true` respectively.
|
||||
- Since we want `Flip` to flip `true` and `false`,
|
||||
fill the first hole with `true` and the second with `false`.
|
||||
- To check things have worked,
|
||||
try `C-c C-d`. (`d` stands for _deduce_.)
|
||||
Then `agda` will ask you to input an expression.
|
||||
Enter `Flip`.
|
||||
In the `*Agda Information*` window,
|
||||
you should see
|
||||
|
||||
```agda
|
||||
Bool → Bool
|
||||
```
|
||||
|
||||
This means `agda` recognises `Flip` as a well-formulated term
|
||||
and is a point in the space of maps from `Bool` to `Bool`.
|
||||
- We can also ask `agda` to compute outputs of `Flip`.
|
||||
Try `C-c C-n` (`n` stands for _normalise_),
|
||||
`agda` should again be asking for an expression.
|
||||
Enter `Flip true`.
|
||||
In the `*Agda Information*` window, you should see `false`, as desired.
|
||||
|
||||
## The isomorphism
|
||||
|
||||
- Navigate to
|
||||
```agda
|
||||
flipIso : Bool ≅ Bool
|
||||
flipIso = {!!}
|
||||
```
|
||||
- Write `iso` in the hole and refine with `C-c C-r`.
|
||||
You should now see
|
||||
```agda
|
||||
flipIso : Bool ≅ Bool
|
||||
flipIso = iso {!!} {!!} {!!} {!!}
|
||||
```
|
||||
- Check that `agda` expects functions `Bool → Bool`
|
||||
to go in the first two holes.
|
||||
These are the maps back and forth which constitute the isomorphism,
|
||||
so fill them with `Flip` and its inverse `Flip`.
|
||||
- Check the goal of the next two holes.
|
||||
They should be
|
||||
```agda
|
||||
section Flip Flip
|
||||
```
|
||||
and
|
||||
```agda
|
||||
retract Flip Flip
|
||||
```
|
||||
This means we need to prove
|
||||
`Flip` is a right inverse and a left inverse of `Flip`.
|
||||
|
||||
- Write the following so that your code looks like
|
||||
```agda
|
||||
flipIso : Bool ≅ Bool
|
||||
flipIso = iso Flip Flip s r where
|
||||
|
||||
s : section Flip Flip
|
||||
s b = {!!}
|
||||
|
||||
r : retract Flip Flip
|
||||
r b = {!!}
|
||||
```
|
||||
The `where` allows you to make definitions local to the current definition,
|
||||
in the sense that you will not be able to access `s` and `r` outside this proof.
|
||||
Note that what follows `where` must be indented.
|
||||
<p>
|
||||
<details>
|
||||
<summary>Skipped step</summary>
|
||||
|
||||
- To find out why we put `s b` on the left you can try
|
||||
```agda
|
||||
flipIso : Bool ≅ Bool
|
||||
flipIso = iso Flip Flip s r where
|
||||
|
||||
s : section Flip Flip
|
||||
s = {!!}
|
||||
|
||||
r : retract Flip Flip
|
||||
r = {!!}
|
||||
```
|
||||
- Check the goal of the hole `s = {!!}` and try using `C-c C-r`.
|
||||
It should give you `λ x → {!!}`.
|
||||
This says it's asking for some new proof for each `x : Bool`.
|
||||
If you check the goal you can find out what proof it wants
|
||||
and that `x : Bool`.
|
||||
- To do a proof for each `x : Bool`, we can also just stick
|
||||
`x` before the `=` and do away with the `λ`.
|
||||
</details>
|
||||
</p>
|
||||
- Check the goal of the hole `s b = {!!}`.
|
||||
In the `*Agda Information*` window, you should see
|
||||
```agda
|
||||
Goal: Flip (Flip b) ≡ b
|
||||
—————————————————————————————————
|
||||
b : Bool
|
||||
```
|
||||
Try to prove this.
|
||||
<p>
|
||||
<details>
|
||||
<summary>Tips</summary>
|
||||
|
||||
You need to case on what `b` can be.
|
||||
Then for the case of `true` and `false`,
|
||||
try `C-c C-r` to see if `agda` can help.
|
||||
|
||||
The added benefit of having `b` before the `=`
|
||||
is exactly this - that we can case on what `b` can be.
|
||||
This is called _pattern matching_.
|
||||
</details>
|
||||
</p>
|
||||
- Do the same for `r b = {!!}`.
|
||||
- Use `C-c C-d` to check that `agda` is okay with `flipIso`.
|
||||
|
||||
## The path
|
||||
|
||||
- Navigate to
|
||||
```agda
|
||||
flipPath : Bool ≡ Bool
|
||||
flipPath = {!!}
|
||||
```
|
||||
- In the hole, write in `isoToPath` and refine with `C-c C-r`.
|
||||
You should now have
|
||||
```agda
|
||||
flipPath : Bool ≡ Bool
|
||||
flipPath = isoToPath {!!}
|
||||
```
|
||||
If you check the new hole, you should see that
|
||||
`agda` is expecting an isomorphism `Bool ≅ Bool`.
|
||||
|
||||
`isoToPath` is the function from the cubical library
|
||||
that converts isomorphisms between spaces
|
||||
into paths between the corresponding points in the space of spaces `Type`.
|
||||
- Fill in the hole with `flipIso`
|
||||
and use `C-c C-d` to check `agda` is happy with `flipPath`.
|
||||
- Try `C-c C-n` with `transport flipPath false`.
|
||||
You should get `true` in the `*Agda Information*` window.
|
||||
|
||||
What `transport` did is it took the path `flipPath` in the
|
||||
space of spaces `Type` and followed the point `false`
|
||||
as `Bool` is transformed along `flipPath`.
|
||||
The end result is of course `true`,
|
||||
since `flipPath` is the path obtained from `flip`!
|
||||
@ -1,101 +0,0 @@
|
||||
# `refl ≡ loop` is empty - 'lifting' paths using the double cover
|
||||
|
||||
By the end of this page we will have shown that
|
||||
`refl ≡ loop` is an empty space.
|
||||
In `1FundamentalGroup/Quest0.agda` locate
|
||||
|
||||
```agda
|
||||
Refl≢loop : Refl ≡ loop → ⊥
|
||||
Refl≢loop h = ?
|
||||
```
|
||||
|
||||
The cubical library has the result
|
||||
`true≢false : true ≡ false → ⊥`
|
||||
which says that the space of paths in `Bool`
|
||||
from `true` to `false` is empty.
|
||||
We will assume it here and leave the proof as a side quest,
|
||||
see `1FundamentalGroup/Quest0SideQuests/SideQuest1`.
|
||||
|
||||
- Load the file with `C-c C-l` and navigate to the hole.
|
||||
- Write `true≢false` in the hole and refine using `C-c C-r`,
|
||||
`agda` knows `true≢false` maps to `⊥` so it automatically
|
||||
will make a new hole.
|
||||
- Check the goal in the new hole using `C-c C-,`
|
||||
it should be asking for a path from `true` to `false`.
|
||||
|
||||
To give this path we need to visualise 'lifting' `Refl`, `loop`
|
||||
and the homotopy `h : Refl ≡ loop`
|
||||
along the Boolean-bundle `doubleCover`.
|
||||
When we 'lift' `Refl` - starting at the point `true : doubleCover base` -
|
||||
it will still be a constant path at `true`,
|
||||
drawn as a dot `true`.
|
||||
When we 'lift' `loop` - starting at the point `true : doubleCover base` -
|
||||
it will look like
|
||||
|
||||
<img src="images/lifted_loops.png"
|
||||
alt="lifted_loops"
|
||||
width="1000"
|
||||
class="center"/>
|
||||
|
||||
The homotopy `h : Refl ≡ loop` is 'lifted'
|
||||
(starting at 'lifted `Refl`')
|
||||
to some kind of surface
|
||||
|
||||
<img src="images/lifted_homotopy.png"
|
||||
alt="lifted_homotopy"
|
||||
width="1000"
|
||||
class="center"/>
|
||||
|
||||
According to the pictures the end point of the 'lifted'
|
||||
`Refl` is `true` and the end point of the 'lifted' `loop` is `false`.
|
||||
We are interested in the end points of each
|
||||
'lifted paths' in the 'lifted homotopy',
|
||||
since this forms a path in the endpoint fiber `doubleCover base`
|
||||
from `true` to `false`.
|
||||
|
||||
We can evaluate the end points of both 'lifted paths' by using
|
||||
something in the cubical library (called `subst`) which we call `endPt`.
|
||||
|
||||
```agda
|
||||
endPt : (B : A → Type) (p : x ≡ y) (bx : B x) → B y
|
||||
```
|
||||
|
||||
<p>
|
||||
<details>
|
||||
<summary>Try interpreting what it says</summary>
|
||||
|
||||
It says given a bundle `B` over space `A`,
|
||||
a path `p` from `x : A` to `y : A`, and
|
||||
a point `bx` above `x`,
|
||||
we can get the end point of 'lifted `p` starting at `bx`'.
|
||||
So let's make the function that takes
|
||||
a path from `base` to `base` and spits out the end point
|
||||
of the 'lifted path' starting at `true`.
|
||||
|
||||
</details>
|
||||
</p>
|
||||
|
||||
```agda
|
||||
endPtOfTrue : (p : base ≡ base) → doubleCover base
|
||||
endPtOfTrue p = ?
|
||||
```
|
||||
|
||||
Try filling in `endPtOfTrue` using `endPt`
|
||||
and the skills you have developed so far.
|
||||
You can verify our expectation that `endPtOfTrue Refl` is `true`
|
||||
and `endPtOfTrue loop` is `false` using `C-c C-n`.
|
||||
|
||||
Lastly we need to make the function `endPtOfTrue`
|
||||
take the path `h : Refl ≡ loop` to a path from `true` to `false`.
|
||||
In general if `f : A → B` is a function and `p` is a path
|
||||
between points `x y : A` then we get a map `cong f p`
|
||||
from `f x` to `f y`.
|
||||
(Note that `p` here is actually a homotopy `h`.)
|
||||
|
||||
```agda
|
||||
cong : (f : A → B) → (p : x ≡ y) → f x ≡ f y
|
||||
```
|
||||
|
||||
Using `cong` and `endPtOfTrue` you should be able to complete `Quest0`.
|
||||
If you have done everything correctly you can reload `agda` and see that
|
||||
you have no remaining goals.
|
||||
@ -1,97 +0,0 @@
|
||||
# Loop Space
|
||||
|
||||
In this quest,
|
||||
we continue to formalise the problem statement.
|
||||
|
||||
> The fundamental group of `S¹` is `ℤ`.
|
||||
|
||||
Intuitively,
|
||||
the fundamental group of `S¹` at `base` is
|
||||
consists of loops based as `base` up to homotopy of paths.
|
||||
In homotopy type theory,
|
||||
we have a native description of loops based at `base` :
|
||||
it is the space `base ≡ base`.
|
||||
|
||||
In general the _loop space_ of a space `A` at a point `a` is defined as follows :
|
||||
|
||||
```agda
|
||||
Ω : (A : Type) (a : A) → Type
|
||||
Ω A a = a ≡ a
|
||||
```
|
||||
|
||||
Clearly for each integer `n : ℤ` we have a path
|
||||
that is '`loop` around `n` times'.
|
||||
Locate `loop_times` in `1FundamentalGroup/Quest1.agda`
|
||||
(note how `agda` treats underscores)
|
||||
|
||||
```agda
|
||||
loop_times : ℤ → Ω S¹ base
|
||||
loop n times = {!!}
|
||||
```
|
||||
|
||||
Try casing on `n`, you should see
|
||||
|
||||
```agda
|
||||
loop_times : ℤ → Ω S¹ base
|
||||
loop pos n times = {!!}
|
||||
loop negsuc n times = {!!}
|
||||
```
|
||||
|
||||
It says to map out of `ℤ` it suffices to
|
||||
map the non-negative integers (`pos`)
|
||||
and the negative integers (`negsuc`).
|
||||
|
||||
```agda
|
||||
data ℤ : Type where
|
||||
pos : (n : ℕ) → ℤ
|
||||
negsuc : (n : ℕ) → ℤ
|
||||
```
|
||||
|
||||
This definition of `ℤ` uses the naturals, so try
|
||||
casing on `n` again, you should see
|
||||
|
||||
```agda
|
||||
loop_times : ℤ → Ω S¹ base
|
||||
loop pos zero times = {!!}
|
||||
loop pos (suc n) times = {!!}
|
||||
loop negsuc n times = {!!}
|
||||
```
|
||||
|
||||
It says to map out of `ℕ` it suffices to map `zero` and
|
||||
map each succesive integer `suc n` inductively.
|
||||
When we loop `zero` (`pos zero`) times what should we get?
|
||||
Try filling it in.
|
||||
For looping `pos (suc n)` times we loop `n` times and
|
||||
loop once more.
|
||||
For this we need composition of paths.
|
||||
|
||||
```agda
|
||||
_∙_ : x ≡ y → y ≡ z → x ≡ z
|
||||
```
|
||||
|
||||
Try typing `_∙_` or `? ∙ ?` in the hole (input `/.`)
|
||||
and refining.
|
||||
Checking the new holes you should see that now you need
|
||||
to give two loops.
|
||||
Try giving it '`loop n times`' composed with `loop`.
|
||||
Then try to also define the map on the negative integers.
|
||||
You will need to invert paths using `sym`.
|
||||
|
||||
```agda
|
||||
sym : x ≡ y → y ≡ x
|
||||
```
|
||||
|
||||
<p>
|
||||
<details>
|
||||
<summary>Looking up definitions</summary>
|
||||
|
||||
If you don't know the definition of something
|
||||
you can look up the definition by sticking your cursor
|
||||
on it and pressing `M-SPC c d` in _insert mode_
|
||||
or `SPC c d` in _evil mode_.
|
||||
|
||||
You can use it to find out the definition of `ℤ` and `ℕ`.
|
||||
|
||||
</details>
|
||||
</p>
|
||||
|
||||
@ -1,129 +0,0 @@
|
||||
# Homotopy Levels
|
||||
|
||||
The loop space can contain higher homotopical information that
|
||||
the fundamental group does not capture.
|
||||
For example, consider `S²`.
|
||||
|
||||
```agda
|
||||
data S² : Type where
|
||||
base : S²
|
||||
loop : base ≡ base
|
||||
northHemisphere : loop ≡ refl
|
||||
southHemisphere : refl ≡ loop
|
||||
```
|
||||
|
||||
<p>
|
||||
<details>
|
||||
<summary>What is `refl`?</summary>
|
||||
|
||||
For any space `A` and point `a : A`,
|
||||
`refl` is the constant path at `a`.
|
||||
Technically speaking, we should write `refl a` to indicate the point we are at,
|
||||
however `agda` is often smart enough to figure that out.
|
||||
</details>
|
||||
</p>
|
||||
|
||||
Intuitively, all loops in `S²` based at `base` is homotopic to
|
||||
the constant path `refl`.
|
||||
In other words, the fundamental group at `base` of `S²` is trivial.
|
||||
However, the 'composition' of the path `southHemisphere` with `northHemisphere`
|
||||
in `base ≡ base` gives the surface of `S²`,
|
||||
which intuitively is not homotopic to the constant point `base`.
|
||||
So `base ≡ base` has non-trivial path structure.
|
||||
|
||||
<img src="images/S2.png"
|
||||
alt="S2"
|
||||
width="1000"
|
||||
class="center"/>
|
||||
|
||||
Let's be more precise about homotopical data :
|
||||
We can check that a space is 'homotopically trivial' (h-trivial)
|
||||
from dimension `n`
|
||||
by checking if spheres of dimension `n` can be filled.
|
||||
To be h-trivial from `0` is for any two points
|
||||
to have a line in between; to fill `S⁰`.
|
||||
This data is captured in
|
||||
|
||||
```agda
|
||||
isProp : Type → Type
|
||||
isProp A = (x y : A) → x ≡ y
|
||||
```
|
||||
|
||||
<p>
|
||||
<details>
|
||||
<summary>All maps are continuous in HoTT</summary>
|
||||
|
||||
There is a subtlety in the definition `isProp`.
|
||||
This 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 that `isProp S¹` is _empty_ despite `S¹` being path connected.
|
||||
|
||||
</details>
|
||||
</p>
|
||||
|
||||
Similarly, to be h-trivial from dimension `1` is for any two points `x y : A`
|
||||
and any two paths `p q : x ≡ y` to have a homotopy from `p` to `q`;
|
||||
to fill `S¹`. This is captured in
|
||||
|
||||
```agda
|
||||
isSet : Type → Type
|
||||
isSet A = (x y : A) → isProp (x ≡ y)
|
||||
```
|
||||
|
||||
To define the fundamental group we will make the loop space satisfy
|
||||
`isSet` by _trucating_ the loop space'.
|
||||
First we show that `isProp S¹` and `isSet S¹` are both empty.
|
||||
Locate `¬isSetS¹` in `1FundamentalGroup/Quest1.agda`.
|
||||
In the cubical library we have the result
|
||||
|
||||
```agda
|
||||
isProp→isSet : (A : Type) → isProp A → isSet A
|
||||
```
|
||||
|
||||
which we will not prove.
|
||||
Assuming `¬isSetS¹`, use `isProp→isSet` to deduce `¬isPropS¹`.
|
||||
<!-- from now you should fill in the hypotheses of the proof yourself -->
|
||||
<!-- (put `h` before the `=` sign or use `C-c C-r`). -->
|
||||
|
||||
<p>
|
||||
<details>
|
||||
<summary>HLevel</summary>
|
||||
|
||||
Generalisation to HLevel and isHLevel n → isHLevel suc n??
|
||||
|
||||
</details>
|
||||
</p>
|
||||
|
||||
Turning our attention to `¬isSetS¹`,
|
||||
again given `h : isSet S¹` -
|
||||
a map continuously taking each pair `x y : A`
|
||||
to a point in `isProp (x ≡ y)`.
|
||||
We can apply `h` twice to the only point `base` available to us,
|
||||
obtaining a point of `isProp (base ≡ base)`.
|
||||
Try mapping from this into the empty space.
|
||||
|
||||
<p>
|
||||
<details>
|
||||
<summary>Hint 0</summary>
|
||||
|
||||
We have already shown that `Refl ≡ loop` is the empty space.
|
||||
We have imported `Quest0Solutions.agda` for you,
|
||||
so you can just quote the result from there.
|
||||
|
||||
</details>
|
||||
</p>
|
||||
|
||||
<p>
|
||||
<details>
|
||||
<summary>Hint 1</summary>
|
||||
|
||||
- assume `h`
|
||||
- type `Refl≢loop` it in the hole and refine
|
||||
- it should now be asking for a proof that `Refl ≡ loop`
|
||||
- try to use `h`
|
||||
|
||||
</details>
|
||||
</p>
|
||||
|
||||
@ -1,3 +0,0 @@
|
||||
# Set Truncation and Higher Homotopy Groups
|
||||
|
||||
We've seen what it means for a space to be a "set".
|
||||
@ -1,101 +0,0 @@
|
||||
# Comparison maps between `Ω S¹ base` and `ℤ`
|
||||
|
||||
In `Quest1` we have defined the map `loop_times : ℤ → Ω S¹ base`.
|
||||
Creating the inverse map is difficult without access to the entire circle.
|
||||
Similarly to how we used `doubleCover` to distinguish `refl` and `base`,
|
||||
the idea is to replace `Bool` with `ℤ`,
|
||||
allowing us to distinguish between all loops on `S¹`.
|
||||
In `Part0` and `Part1` we will construct one of the two comparison maps
|
||||
across the whole circle, called `spinCount`.
|
||||
|
||||
The plan is :
|
||||
|
||||
1. Define a function `sucℤ : ℤ → ℤ` that increases every integer by one
|
||||
2. Prove that `sucℤ` is an isomorphism by constructing
|
||||
an inverse map `predℤ : ℤ → ℤ`.
|
||||
3. Turn `sucℤ` into a path `sucPath : ℤ ≡ ℤ` using `isoToPath`
|
||||
4. Define `helix : S¹ → Type` by mapping `base` to `ℤ` and
|
||||
a generic point `loop i` to `sucPath i`.
|
||||
<<<<<<< HEAD
|
||||
5. Use `helix` and `endPt` to define the map `base ≡ x → helix x`
|
||||
on all `x : S¹`, in particular giving us `Ω S¹ base → ℤ`
|
||||
when applied to `base`.
|
||||
|
||||
In this part, we focus on `1` and `2`.
|
||||
=======
|
||||
5. Use `helix` and `endPt` to define the map
|
||||
`spinCountBase : base ≡ base → ℤ`
|
||||
Intuitively it counts how many times a path loops around `S¹`.
|
||||
a generic point `loop i` to `sucPath i`.
|
||||
6. Generalize this across the circle.
|
||||
|
||||
In this part, we focus on `1`, `2` and `3`.
|
||||
>>>>>>> df5d7c381b1adae1d2547df95f5d73bcf3447ac4
|
||||
|
||||
## `sucℤ`
|
||||
|
||||
- Setup the definition of `sucℤ` so that it looks of the form :
|
||||
```agda
|
||||
Name : TypeOfSpace
|
||||
Name inputs = ?
|
||||
```
|
||||
|
||||
Compare it with our solutions in `1FundamentalGroup/Quest1.agda`
|
||||
- We will define `sucℤ` the same way we defined `loop_times` :
|
||||
by induction.
|
||||
Do cases on the input of `sucℤ`.
|
||||
You should have something like :
|
||||
```agda
|
||||
sucℤ : ℤ → ℤ
|
||||
sucℤ pos n = ?
|
||||
sucℤ negsuc n = ?
|
||||
```
|
||||
- For the non-negative integers `pos n` we want to map to its successor.
|
||||
Recall that the `n` here is a point of the naturals `ℕ` whose definition is :
|
||||
```agda
|
||||
data ℕ : Type where
|
||||
zero : ℕ
|
||||
suc : ℕ → ℕ
|
||||
```
|
||||
Use `suc` to map `pos n` to its successor.
|
||||
- The negative integers require a bit more care.
|
||||
Recall that annoyingly `negsuc n` means "`- (n + 1)`".
|
||||
We want to map `- (n + 1)` to `- n`.
|
||||
Try doing this.
|
||||
Then realise "you run out of negative integers at `-(0 + 1)`"
|
||||
so you must do cases on `n` and treat the `-(0 + 1)` case separately.
|
||||
<p>
|
||||
<details>
|
||||
<summary>Hint</summary>
|
||||
|
||||
Do `C-c C-c` on `n`.
|
||||
Then map `negsuc 0` to `pos 0`.
|
||||
For `negsuc (suc n)`, map it to `negsuc n`.
|
||||
|
||||
</details>
|
||||
</p>
|
||||
- This completes the definition of `sucℤ`.
|
||||
Use `C-c C-n` to check it computes correctly.
|
||||
E.g. check that `sucℤ (- 1)` computes to `pos 0`
|
||||
and `sucℤ (pos 0)` computes to `pos 1`.
|
||||
|
||||
## `sucℤ` is an isomorphism
|
||||
|
||||
- The goal is to define `predℤ : ℤ → ℤ` which
|
||||
"takes `n` to its predecessor `n - 1`".
|
||||
This will act as the (homotopical) inverse of `sucℤ`.
|
||||
Now that you have experience from defining `sucℤ`,
|
||||
try defining `predℤ`.
|
||||
- Imitating what we did with `flipIso` and
|
||||
give a point `sucℤIso : ℤ ≅ ℤ`
|
||||
by using `predℤ` as the inverse and proving
|
||||
<<<<<<< HEAD
|
||||
`section sucℤ predℤ` and `retract sucℤ predℤ`.
|
||||
=======
|
||||
`section sucℤ predℤ` and `retract sucℤ predℤ`.
|
||||
|
||||
## `sucℤ` is a path
|
||||
|
||||
- Imitating what we did with `flipPath`,
|
||||
upgrade `sucℤIso` to `sucℤPath`.
|
||||
>>>>>>> df5d7c381b1adae1d2547df95f5d73bcf3447ac4
|
||||
@ -1,54 +0,0 @@
|
||||
# Comparison maps between `Ω S¹ base` and `ℤ` - `spinCount`
|
||||
|
||||
## The `ℤ`-bundle `helix`
|
||||
|
||||
We want to make a `ℤ`-bundle over `S¹` by
|
||||
'copying ℤ across the loop via `sucℤPath`'.
|
||||
In `Quest2.agda` locate
|
||||
|
||||
```agda
|
||||
helix : S¹ → Type
|
||||
helix = {!!}
|
||||
```
|
||||
|
||||
Try to imitate the definition of `doubleCover` to define the bunlde `helix`.
|
||||
You should compare your definition to ours in `Quest2Solutions.agda`.
|
||||
Note that we have called this `helix`, since the picture of this `ℤ`-bundle
|
||||
looks like
|
||||
|
||||
<img src="images/helix.png"
|
||||
alt="helix"
|
||||
width="1000"
|
||||
class="center"/>
|
||||
|
||||
## Counting loops
|
||||
|
||||
Now we can do what was originally difficult - constructing an inverse map
|
||||
(over all points).
|
||||
Now we want to be able to count how many times a path `base ≡ base` loops around
|
||||
`S¹`, which we can do now using `helix` and finding end points of 'lifted' paths.
|
||||
For example the path `loop` should loop around once,
|
||||
counted by looking at the end point of 'lifted' `loop`, starting at `0`.
|
||||
Hence try to define
|
||||
|
||||
```agda
|
||||
spinCountBase : base ≡ base → helix base
|
||||
spinCountBase = {!!}
|
||||
```
|
||||
|
||||
Try computing a few values using `C-c C-n`,
|
||||
you can try it on `refl`, `loop`, `loop 3 times`, `loop (- 1) times` and so on.
|
||||
|
||||
## Generalising
|
||||
|
||||
The function `spinCountBase`
|
||||
can actually be improved without any extra work to a function on all of `S¹`
|
||||
|
||||
```agda
|
||||
spinCount : (x : S¹) → base ≡ x → helix x
|
||||
spinCount = {!!}
|
||||
```
|
||||
|
||||
We will show that this and a general version of `loop_times` are
|
||||
inverses of each other over `S¹`, in particular obtaining an isomorphism
|
||||
between `base ≡ base` and `ℤ`.
|
||||
@ -1,44 +0,0 @@
|
||||
# George feedback
|
||||
|
||||
## Subject info
|
||||
|
||||
[] has some experience with type theory and haskell
|
||||
|
||||
## Quest0/Part0
|
||||
|
||||
[x] clarify the notation `a : A`
|
||||
[x] hide the imports
|
||||
[x] definition of inductive type doesn't make sense
|
||||
without the further details.
|
||||
[x] confusion of `{!!}` and `{0}` and `?`
|
||||
[x] comparing holes to agda-info window is intuitive
|
||||
[x] error on firsts refine
|
||||
[x] add at each step what the agda-info window looks like
|
||||
[x] confusion about hole numbers. "just ignore them"
|
||||
[x] subject tries to read constraint in agda-info window.
|
||||
Shld deal with this somehow.
|
||||
[] emphasize no need to fill holes in order.
|
||||
|
||||
## Quest0/Part1
|
||||
|
||||
[x] subject confused about 'space of spaces'.
|
||||
More specifically, need to say `a : A` means "`a` is a point of the space `A`".
|
||||
[x] we shld say `a ≡ b` means space of paths from `a` to `b`.
|
||||
[-] 'contradiction' is a pre-existing concept in subject brain.
|
||||
[x] "not sure that helps" - subject about definition of `Bool`
|
||||
[x] "is `flipPath` taking a point from `Bool` to another point of `Bool`
|
||||
or is it taking a space to another space?"
|
||||
[] "just some terminology" - subject on the definition of _fiber_.
|
||||
Subject did not take in the picture of what it is called fiber.
|
||||
[-] need to add earlier how to check goal of holes.
|
||||
[x] need to be clear _we are assuming `flipPath` is constructed already_.
|
||||
[x] overall : need to be clearer that `Type` is space of spaces,
|
||||
and paths in `Type` are saying which spaces are the same.
|
||||
|
||||
## Quest0/Part2
|
||||
|
||||
[x] For the `iso` bit, change to just `C-c C-r` cuz `Iso` only has one constructor.
|
||||
[x] say you can check def of `Iso` by using `SPC c d`
|
||||
[x] say "just write `s` and `r` and write the rest then load".
|
||||
[x] emphasize agda is indentation sensitive.
|
||||
[x] subject unexpectedly extracts lemma `true ≡ true`.
|
||||
@ -1,33 +0,0 @@
|
||||
Fundamental Group of S¹
|
||||
================
|
||||
|
||||
Prerequisites :
|
||||
- circle
|
||||
- loop space
|
||||
- have useless maps pi(S¹) → ℤ and ℤ → pi(S¹)
|
||||
|
||||
|
||||
|
||||
|
||||
- we make helix from ℤ ≡ ℤ
|
||||
|
||||
-
|
||||
|
||||
Motivating Steps :
|
||||
0. After sufficient pondering, you guess that
|
||||
loops are determined by how many times they go around
|
||||
1. Count number of times loops go around using ℤ
|
||||
by setting the single loop to +1.
|
||||
2. You can make a comparison maps between loop space and ℤ
|
||||
but can't yet show an equivalence
|
||||
3. You realize you need to use the definition of S¹,
|
||||
so you go from `base ≡ base ≃ Z` to `base ≡ x ≃ Bundle x`.
|
||||
i.e. You try to make the equivalence _over_ S¹
|
||||
|
||||
|
||||
Random thought :
|
||||
to prove `a = b`, we realise that `a = f(x0)`
|
||||
and `b = g(x0)` for `x0 : X`,
|
||||
and instead show `(x : X) → f x = g x`.
|
||||
This turns out to be easier since we now get
|
||||
access to the recursor of `X`.
|
||||
Loading…
Reference in New Issue
Block a user