diff --git a/1FundamentalGroup/Quest0.agda b/1FundamentalGroup/Quest0.agda index a8c4364..520eaa7 100644 --- a/1FundamentalGroup/Quest0.agda +++ b/1FundamentalGroup/Quest0.agda @@ -29,6 +29,9 @@ Flip : Bool → Bool Flip false = true Flip true = false +-- notice we used `refl` instead of `λ i → false`, +-- you might want to find out what `refl` does +-- by looking up the definition flipIso : Bool ≅ Bool flipIso = iso Flip Flip s r where s : section Flip Flip @@ -85,7 +88,7 @@ endPtOfTrue p = endPt doubleCover p true {- -You can check that `SubstTrue refl` and `SubstTrue loop` +You can check that `SubstTrue Refl` and `SubstTrue loop` are using `C-c C-n` -} @@ -102,10 +105,10 @@ gives us a path in `B` from `f x` to `f y` We can use the above to get the contradiction we want by -- assuming `p : refl ≡ loop` -- deducing `SubstTrue refl ≡ SubstTrue loop` using `cong` +- assuming `p : Refl ≡ loop` +- deducing `SubstTrue Refl ≡ SubstTrue loop` using `cong` -} -refl≢loop : refl ≡ loop → ⊥ -refl≢loop p = true≢false (cong endPtOfTrue p) +Refl≢loop : Refl ≡ loop → ⊥ +Refl≢loop p = true≢false (cong endPtOfTrue p) diff --git a/1FundamentalGroup/Quest0Part0.md b/1FundamentalGroup/Quest0Part0.md index c49fcc7..14898b9 100644 --- a/1FundamentalGroup/Quest0Part0.md +++ b/1FundamentalGroup/Quest0Part0.md @@ -9,8 +9,8 @@ We begin by formalising the problem statement. A contruction of 'the circle' is : -- a point -- an edge from that point to itself +- a point called `base` +- an edge from that point to itself called `loop` Here is our definition of the circle in `agda`. @@ -23,6 +23,27 @@ data S¹ : Type where 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. + +

+

+Further details + +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 + +
+

An "edge" is the same as a path. There are other paths in `S¹`, @@ -83,6 +104,8 @@ We will fill the hole `{ }0`. - 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` diff --git a/1FundamentalGroup/Quest0Part1.md b/1FundamentalGroup/Quest0Part1.md index b2665bb..c3bf512 100644 --- a/1FundamentalGroup/Quest0Part1.md +++ b/1FundamentalGroup/Quest0Part1.md @@ -1,13 +1,7 @@ -# `refl ≡ loop` is empty - -To get a better feel of `S¹`, we show that the space - -``` -refl ≡ loop -``` - -is empty. +# `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` : @@ -15,20 +9,20 @@ Here is what this looks like in `agda` : data ⊥ : Type where ``` -This says "the empty space is a space with no points in it". +This says "the empty space `⊥` is a space with no points in it". -Here are two candidate definitions for a space `A` to be empty : +Here are three candidate definitions for a space `A` to be empty : -- there is a point `f : A → ⊥` -- there is a path `p : A ≡ ⊥` in the space of spaces `Type` +- 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', +These turn out to be 'the same' (see `1FundamentalGroup/Quest0SideQuests/SideQuest0`), however for our present purposes we will use the first definition. -So our goal now is to produce a point of +Our goal is therefore to produce a point in the function space ```agda -( refl ≡ loop ) → ⊥ +( Refl ≡ loop ) → ⊥ ``` The authors of this series have thought long and hard @@ -36,12 +30,14 @@ 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 create a map from `refl ≡ loop` to `true ≡ false` by +> 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 ) → ⊥`. +> 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. @@ -51,6 +47,13 @@ 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 +(Insert picture of 'lift' of `loop`) + Let's assume for the moment that we have `flipPath` already and define `doubleCover`. @@ -62,6 +65,7 @@ define `doubleCover`. ``` - 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 @@ -70,9 +74,9 @@ define `doubleCover`. doubleCover (loop i) = {!!} ``` - The meaning is as follows : - the circle is made from a point `base` together with an edge `loop`, - so a map out of it to a space is the same as choosing + 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. @@ -85,5 +89,7 @@ define `doubleCover`. 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! diff --git a/1FundamentalGroup/Quest0Part2.md b/1FundamentalGroup/Quest0Part2.md index 417dd8c..a06c71e 100644 --- a/1FundamentalGroup/Quest0Part2.md +++ b/1FundamentalGroup/Quest0Part2.md @@ -1,4 +1,4 @@ -# `refl ≡ loop` is empty - Defining `flipPath` via Univalence +# `Refl ≡ loop` is empty - Defining `flipPath` via Univalence In this part, we will define the path `flipPath : Bool ≡ Bool`. Recall the picture of `doubleCover`. @@ -12,13 +12,13 @@ We proceed in steps : 1. Define the function `Flip : Bool → Bool`. 2. Promote this to an isomorphism `flipIso : Bool ≅ Bool`. -3. The intuition is that the univalence axiom asserts that - paths in the space of spaces correspond to +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 of types. - We use this to turn `flipIso` into - a path `flipPath : Bool ≡ Bool`. + we can make paths in `Type` from isomorphisms in `Type`. ## The function @@ -29,18 +29,17 @@ We proceed in steps : Flip x = {!!} ``` - Write `x` inside the hole, - and do `C-c C-c` with your cursor still inside. - The `c` stands for _cases_. + and do `C-c C-c` with your cursor still inside. You should now see : ```agda Flip : Bool → Bool Flip false = {!!} Flip true = {!!} ``` - What this is saying is that + This means : the space `Bool` is made of two points `false, true` and nothing else, - so to map out of it, - it suffices to give something to map `false` and `true` to respectively. + 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, @@ -57,7 +56,7 @@ We proceed in steps : 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_.) + 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. @@ -75,10 +74,10 @@ We proceed in steps : flipIso : Bool ≅ Bool flipIso = iso {!!} {!!} {!!} {!!} ``` -- Check that what `agda` is expecting in the first two holes - are functions `Bool → Bool`. - These are our maps back and forth which will constitute the isomorphism - so write `Flip` and `Flip` in the first two holes. +- 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 @@ -90,6 +89,7 @@ We proceed in steps : ``` 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 @@ -104,6 +104,30 @@ We proceed in steps : 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. +

+

+ Skipped step + +- 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 `λ`. +
+

- Check the goal of the hole `s b = {!!}`. In the `*Agda Information*` window, you should see ```agda @@ -111,14 +135,20 @@ We proceed in steps : ————————————————————————————————— b : Bool ``` + This says it suffices to find a path from `Flip (Flip b)` to `b` + in the space `Bool`. Try to prove this.

- Hint + Tips - You need to do cases on what `b` can be. + 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_.

- Do the same for `r b = {!!}`. diff --git a/1FundamentalGroup/Quest0Part3.md b/1FundamentalGroup/Quest0Part3.md index 740dd3c..79a152c 100644 --- a/1FundamentalGroup/Quest0Part3.md +++ b/1FundamentalGroup/Quest0Part3.md @@ -1,23 +1,20 @@ -# `refl ≡ loop` is empty - transporting paths using the double cover +# `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, -we start at the end, moving backwards to what we need, -as we would often do in practice. - -In `Quest0.agda` you should see +`refl ≡ loop` is an empty space. +In `1FundamentalGroup/Quest0.agda` locate ```agda Refl≢loop : Refl ≡ loop → ⊥ Refl≢loop h = ? ``` -In the library we have +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 it as a side quest, -see `1FundamentalGroup/Quest0SideQuests/SideQuest0`. +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`, @@ -26,42 +23,54 @@ see `1FundamentalGroup/Quest0SideQuests/SideQuest0`. - 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` and `loop` +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`, -which we can just draw as a dot `true`. +drawn as a dot `true`. When we 'lift' `loop` - starting at the point `true : doubleCover base` - it will look like -We can find the end points of both 'lifted paths' by using `subst`. -We should be able to see that the end point of the 'lifted' -`Refl` is just `true` and the end point of the 'lifted' `loop` is `false`. -Now a homotopy `h : refl ≡ loop` is 'lifted' to some kind of surface +The homotopy `h : refl ≡ loop` is 'lifted' +(starting at 'lifted `refl`') +to some kind of surface -The end points of each 'lifted paths' in the 'lifted homotopy' -form a path in the endpoint fiber `doubleCover base` -from the endpoint of 'lifted `Refl`' to the endpoint of 'lifted `base`', -i.e. a path from `true` to `false` in `Bool`, which is what we need. +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 use `endPt` to pick out the end points of 'lifted paths', -given to us in the library (originally called `subst`): + + +We can evaluate the end points of both 'lifted paths' by using +something in the cubical library called `endPt` +(originally called `subst`). ```agda endPt : (B : A → Type) (p : x ≡ y) (bx : B x) → B y ``` +

+

+Try interpreting what it says + 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'. +of the 'lifted path' starting at `true`. + +
+

```agda endPtOfTrue : (p : base ≡ base) → doubleCover base @@ -70,8 +79,8 @@ endPtOfTrue p = ? Try filling in `endPtOfTrue` using `endPt` and the skills you have developed so far. -You can check that `endPtOfTrue Refl` is `true` -and that `endPtOfTrue loop` is `false` using `C-c C-n`. +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`. @@ -85,3 +94,5 @@ 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. diff --git a/EmacsCommands.md b/EmacsCommands.md index 6646570..099e8e5 100644 --- a/EmacsCommands.md +++ b/EmacsCommands.md @@ -13,11 +13,16 @@ Example `C-c C-l` in Agda files is `Ctrl-c`, let go, `Ctrl-l` ## General Doom Emacs usage +The 'ambient mode' is called __evil mode_ and follows +vim-like bindings. +The following commands are for _evil mode_: + - `SPC h b b` to look for bindings - `SPC f f` to find files. can use `TAB` for auto-completing paths - `h j k l` for left down up right - `SPC b k` to kill 'buffers' -- `i` to go into 'insert' and `ESC` or `C-g` to escape 'insert'. +- `i` to go into __insert mode_ (in insert mode you can insert text) + and `ESC` or `C-g` to go back to _evil mode_. - `C-_` to undo For beta users, to get the latest patch @@ -28,6 +33,7 @@ For beta users, to get the latest patch ## Agda usage +To insert text in the `agda` file use `i` to enter _insert mode_. - `C-c C-l` loads the file - `C-c C-,` checks goal of the hole your cursor is in. @@ -37,5 +43,5 @@ For beta users, to get the latest patch - `C-c C-d` used for checking types of terms - `C-c C-n` used for 'reducing' terms to their 'simplest form' - `C-c C-.` does `C-c C-,` and `C-c C-d` - +- `M-SPC c d` looks up the definition of the thing you are hovering over. diff --git a/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai b/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai index 437f5f2..f035d4c 100644 Binary files a/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai and b/_build/2.6.2/agda/1FundamentalGroup/Quest0.agdai differ