diff --git a/1FundamentalGroup/Quest0.agda b/1FundamentalGroup/Quest0.agda index 2fdf1a9..fd12ba5 100644 --- a/1FundamentalGroup/Quest0.agda +++ b/1FundamentalGroup/Quest0.agda @@ -4,7 +4,7 @@ open import Cubical.Data.Empty open import Cubical.Data.Unit renaming ( Unit to ⊤ ) open import Cubical.Data.Bool open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Isomorphism renaming ( Iso to _≅_ ) open import Cubical.Foundations.Path private @@ -15,68 +15,8 @@ data S¹ : Type where base : S¹ loop : base ≡ base --- if you don't know how to input a character --- go to evil-mode, put your cursor on the character --- and do `SPC h '` - -¬ : Type u → Type u -¬ A = A → ⊥ - -_≢_ : {A : Type u} → (x y : A) → Type u -x ≢ y = ¬ (x ≡ y) - -_≅_ = Iso - -{- Bool - -data Bool : Type where - true : Bool - false : Bool - -The above definition for the Booleans -can be interpreted as - -- a construction with only two recipes - `true` and `false` -- a space with two points `true` and `false`. - This space is discrete in the sense that - we haven't specified any paths. - -Our goal is to show - - refl ≢ loop (input \nequiv) - -that there is path (aka homotopy) from `refl` to `loop`. -To do so we must assume there is such a path and derive -a contradiction. -The contradiction we will try to reach is that `true ≡ false`. -Indeed it does not hold: - --} - - -{- transport - -To follow a point in `a : A` along a path `p : A ≡ B` -we use - - transport : {A B : Type u} → A ≡ B → A → B - -Why do we propify? Discuss. - --} - -true≢false' : true ≢ false -true≢false' h = transport ⊤≡⊥ tt where - - propify : Bool → Type - propify false = ⊥ - propify true = ⊤ - - ⊤≡⊥ : ⊤ ≡ ⊥ - ⊤≡⊥ = cong propify h - - +Refl : base ≡ base +Refl = λ i → base Flip : Bool → Bool Flip false = true @@ -157,7 +97,6 @@ with the fiber we set for `base`, which is `Bool`. doubleCover : S¹ → Type doubleCover base = Bool doubleCover (loop i) = flipPath i - {- subst Given a bundle `B : A → Type u` @@ -205,5 +144,5 @@ by -} -refl≢loop : refl ≢ loop +refl≢loop : refl ≡ loop → ⊥ refl≢loop p = true≢false (cong SubstTrue p) diff --git a/1FundamentalGroup/Quest0.md b/1FundamentalGroup/Quest0.md deleted file mode 100644 index 36f5a69..0000000 --- a/1FundamentalGroup/Quest0.md +++ /dev/null @@ -1,29 +0,0 @@ -Whoa very cool -======================= - -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. - - - -## The Circle - -A contruction of 'the circle' is : - -- a point -- an edge from that point to itself - -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`_. -An "edge" is the same as a path. - diff --git a/1FundamentalGroup/Quest0Part0.md b/1FundamentalGroup/Quest0Part0.md new file mode 100644 index 0000000..65138a9 --- /dev/null +++ b/1FundamentalGroup/Quest0Part0.md @@ -0,0 +1,88 @@ +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 +- an edge from that point to itself + +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. + +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` locate `Refl : base ≡ base`, +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. +- 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 new file mode 100644 index 0000000..b2665bb --- /dev/null +++ b/1FundamentalGroup/Quest0Part1.md @@ -0,0 +1,89 @@ +# `refl ≡ loop` is empty + +To get a better feel of `S¹`, we show that the space + +``` +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 two 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 an isomorphism `i : A ≅ ⊥` of spaces + +These turn out to be 'the same', +however for our present purposes we will use the first definition. +So our goal now is to produce a point of + +```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 create a map from `refl ≡ loop` to `true ≡ false` 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`. +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. +(Insert gif of double cover.) +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_. + +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`. + You should now see two new holes : + + ```agda + doubleCover : S¹ → Type + doubleCover base = {!!} + 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 + 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. + +Defining `flipPath` is quite involved and we will do so in the next quest! diff --git a/1FundamentalGroup/Quest0SideQuests/SideQuest0.agda b/1FundamentalGroup/Quest0SideQuests/SideQuest0.agda new file mode 100644 index 0000000..fac13ea --- /dev/null +++ b/1FundamentalGroup/Quest0SideQuests/SideQuest0.agda @@ -0,0 +1,26 @@ +module 1FundamentalGroup.Quest0SideQuests.SideQuest0 where + +open import Cubical.Data.Empty +open import Cubical.Data.Unit renaming ( Unit to ⊤ ) +open import Cubical.Data.Bool +open import Cubical.Foundations.Prelude + +true≢false' : true ≡ false → ⊥ +true≢false' h = transport ⊤≡⊥ tt where + + propify : Bool → Type + propify false = ⊥ + propify true = ⊤ + + ⊤≡⊥ : ⊤ ≡ ⊥ + ⊤≡⊥ = cong propify h +{- transport + +To follow a point in `a : A` along a path `p : A ≡ B` +we use + + transport : {A B : Type u} → A ≡ B → A → B + +Why do we propify? Discuss. + +-} diff --git a/Installation/Mac.md b/Installation/Mac.md index 917b9db..b328fa6 100644 --- a/Installation/Mac.md +++ b/Installation/Mac.md @@ -6,6 +6,9 @@ Installing TheHoTTGame on MacOS `brew link --overwrite git` `rm -r .emacs.d` +`export PATH="/usr/local/bin:$PATH"` +in `.bash_profile` (if old) + ``` # required dependencies brew install git ripgrep @@ -28,4 +31,12 @@ brew install emacs-mac --with-modules --with-emacs-sexy-icon --with-no-title-bar # Make an app link in Applications ln -s /usr/local/opt/emacs-mac/Emacs.app /Applications/Emacs.app + +# doom emacs +git clone https://github.com/hlissner/doom-emacs ~/.emacs.d +~/.emacs.d/bin/doom install + +# so that you can use 'doom' anywhere +export PATH=”$HOME/.emacs.d/bin:$PATH” + ``` diff --git a/_build/2.6.3/agda/1FundamentalGroup/Quest0.agdai b/_build/2.6.3/agda/1FundamentalGroup/Quest0.agdai new file mode 100644 index 0000000..99fa681 Binary files /dev/null and b/_build/2.6.3/agda/1FundamentalGroup/Quest0.agdai differ diff --git a/_build/2.6.3/agda/1FundamentalGroup/Quest0SideQuests/SideQuest0.agdai b/_build/2.6.3/agda/1FundamentalGroup/Quest0SideQuests/SideQuest0.agdai new file mode 100644 index 0000000..6594de6 Binary files /dev/null and b/_build/2.6.3/agda/1FundamentalGroup/Quest0SideQuests/SideQuest0.agdai differ