This commit is contained in:
kl-i 2021-09-22 11:26:03 +01:00
commit 70fd1aa024
6 changed files with 145 additions and 20 deletions

View File

@ -0,0 +1,47 @@
module 1FundamentalGroup.Quest2 where
open import Cubical.Core.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Int using ( ; pos ; negsuc ; -_)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude renaming (subst to endPt)
open import Cubical.HITs.S1 using ( ; base ; loop)
open import 1FundamentalGroup.Quest1
suc :
suc (pos n) = pos (suc n)
suc (negsuc zero) = pos zero
suc (negsuc (suc n)) = negsuc n
pred :
pred (pos zero) = negsuc zero
pred (pos (suc n)) = pos n
pred (negsuc n) = negsuc (suc n)
sucIso : Iso
sucIso = iso suc pred s r where
s : section suc pred
s (pos zero) = refl
s (pos (suc n)) = refl
s (negsuc zero) = refl
s (negsuc (suc n)) = refl
r : retract suc pred
r (pos zero) = refl
r (pos (suc n)) = refl
r (negsuc zero) = refl
r (negsuc (suc n)) = refl
sucPath :
sucPath = isoToPath sucIso
helix : Type
helix base =
helix (loop i) = sucPath i
spinCountBase : base base
spinCountBase p = endPt helix p 0
spinCount : (x : ) base x helix x
spinCount x p = endPt helix p 0

View File

@ -5,6 +5,8 @@ Creating the inverse map is difficult without access to the entire circle.
Similarly to how we used `doubleCover` to distinguish `refl` and `base`, Similarly to how we used `doubleCover` to distinguish `refl` and `base`,
the idea is to replace `Bool` with ``, the idea is to replace `Bool` with ``,
allowing us to distinguish between all loops on `S¹`. 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 : The plan is :
@ -14,11 +16,21 @@ The plan is :
3. Turn `suc` into a path `sucPath : ` using `isoToPath` 3. Turn `suc` into a path `sucPath : ` using `isoToPath`
4. Define `helix : S¹ → Type` by mapping `base` to `` and 4. Define `helix : S¹ → Type` by mapping `base` to `` and
a generic point `loop i` to `sucPath i`. a generic point `loop i` to `sucPath i`.
<<<<<<< HEAD
5. Use `helix` and `endPt` to define the map `base ≡ x → helix x` 5. Use `helix` and `endPt` to define the map `base ≡ x → helix x`
on all `x : S¹`, in particular giving us `Ω S¹ base → ` on all `x : S¹`, in particular giving us `Ω S¹ base → `
when applied to `base`. when applied to `base`.
In this part, we focus on `1` and `2`. 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` ## `suc`
@ -77,4 +89,13 @@ In this part, we focus on `1` and `2`.
- Imitating what we did with `flipIso` and - Imitating what we did with `flipIso` and
give a point `sucIso : ` give a point `sucIso : `
by using `pred` as the inverse and proving by using `pred` as the inverse and proving
<<<<<<< HEAD
`section suc pred` and `retract suc pred`. `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 `sucIso` to `sucPath`.
>>>>>>> df5d7c381b1adae1d2547df95f5d73bcf3447ac4

View File

@ -0,0 +1,54 @@
# Comparison maps between `Ω S¹ base` and `` - `spinCount`
## The ``-bundle `helix`
We want to make a ``-bundle over `S¹` by
'copying across the loop via `sucPath`'.
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 ``.

View File

@ -43,26 +43,29 @@ Try opening `Trinitarianism/Quest0.agda` in Emacs
and do `Ctrl-c Ctrl-l`. and do `Ctrl-c Ctrl-l`.
Some text should be highlighted, and any `?` should turn into `{ }`. Some text should be highlighted, and any `?` should turn into `{ }`.
## How the game works ## Where to start?
Our Game is currently under development. You can start with `0Trinitarianism` if you are interested in
As of now you can try the _quests_ in the `Trinitarianism` folder. how logic, type theory and category theory come together
Each quest consists of three files, for example : as different ways to view the same thing.
- `Trinitarianism/Quest0.md` is the guide for the quest. If you are more interested in homotopy theory,
In there, you will find details of the tasks try `1FundamentalGroup` where we show that the
you must finish in order to complete the quest. fundamental group of `S¹` is ``.
For now, it is recommended that
you view these online within github.
- `Trinitarianism/Quest0.agda` is the agda file in which
you do the quest.
- `Trinitarianism/Quest0Solutions.agda` contains
solutions to the tasks in the quest.
## Emacs and Agda usage ## How to start?
We have a file with a list of [basic Emacs commands](
To start with `1FundamentalGroup` (for example),
find the GitHub page [`1FundamentalGroup/Quest0Part0.md`](
https://github.com/thehottgame/TheHoTTGame/blob/main/1FundamentalGroup/Quest0Part0.md
)
and follow the instructions there,
then trying the following files in the same directory.
Open up the corresponding `.agda` file in `emacs` to
follow along with the instructions in the quests.
## Emacs issues
If you can't figure out `emacs` or forget some command, then
try consulting our guide for [basic Emacs commands](
https://github.com/thehottgame/TheHoTTGame/blob/main/EmacsCommands.md https://github.com/thehottgame/TheHoTTGame/blob/main/EmacsCommands.md
), ).
but you _should_ be able to learn how to use Agda as you go along.
## Feedback
If you have any feedback please contact the devs.

Binary file not shown.