diff --git a/README.md b/README.md index 9b097e7..8465b57 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,11 @@ The HoTT Game ============= -The Homotopy Type Theory (HoTT) Game is a project aimed at -introducing mathematicians with no experience -in proof verification interested in HoTT and able to use Agda for HoTT. -This guide will help you get the Game working for you. +The Homotopy Type Theory (HoTT) Game is a project written by mathematicians +for mathematicians interested in HoTT and no experience in proof verification, +with the aim of introducing Cubical Agda as a tool for +trying out mathematics in HoTT. +This page will help you get the Game working for you. ## Installing Agda and the Cubical Agda library @@ -15,8 +16,8 @@ It is recommended that you use Agda in the text editor [emacs]( https://www.gnu.org/software/emacs/tour/index.html), in particular -[Doom Emacs](https://github.com/hlissner/doom-emacs) is a bit nicer if you -can't be bothered to do a bunch of configuration. +[Doom Emacs](https://github.com/hlissner/doom-emacs), +if you can't be bothered to do a bunch of configuration. Once you have Emacs and Agda, get the [Cubical Library]( https://github.com/agda/cubical) (version 0.3) @@ -38,19 +39,28 @@ the-directory/HoTTGameLib.agda ``` to your `libraries` file as above. -Try opening up `Trinitarianism/AsProps/Quest0.agda` in Emacs -and do `Ctrl-c Ctrl-l`. +Try opening `Trinitarianism/Quest0.agda` in Emacs +and do `Ctrl-c Ctrl-l`. Some text should be highlighted, and any `?` should turn into `{ }`. ## How the game works Our Game is under development. Please contact the devs. -Currently you can try `Trinitarianism/AsProps/Quest0.agda`, -making use of the accompanying solutions Agda file. +Currently you can try the _quests_ in the `Trinitarianism` folder. +Each quest consists of three files, for example : +- `Trinitarianism/Quest0.md` is the guide for the quest + In there, you will find details of the tasks + you must finish in order to complete the quest. + For now, it is recommended that + you view these online within github. +- `Trinitarianism/Quest0.agda` is the actual file in which + you do the quest. +- `Trinitarianism/Quest0Solutions.agda` contains + solutions to the tasks in the quest. ## Emacs and Agda usage -We have a file with a list of basic Emacs commands and -you _should_ be able to learn how to use Agda as you go along. +We will have a file with a list of basic Emacs commands, +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. diff --git a/Trinitarianism/.DS_Store b/Trinitarianism/.DS_Store new file mode 100644 index 0000000..5008ddf Binary files /dev/null and b/Trinitarianism/.DS_Store differ diff --git a/Trinitarianism/Quest0.md b/Trinitarianism/Quest0.md index be77259..807e0f4 100644 --- a/Trinitarianism/Quest0.md +++ b/Trinitarianism/Quest0.md @@ -13,10 +13,10 @@ we have another type `A → B : Type` which can be seen as - internal hom of the category `Type` To give examples of this, let's make some types first! +Here is how we define 'true'. ```agda --- Here is how we define 'true' -data ⊤ : Type u where +data ⊤ : Type where tt : ⊤ ``` @@ -40,14 +40,14 @@ TrueToTrue : ⊤ → ⊤ TrueToTrue = {!!} ``` - - press `C-c C-l` (this means `Ctrl-c Ctrl-l`) to load the document, - and now you can fill the holes + - enter `C-c C-l` (this means `Ctrl-c Ctrl-l`) to load the document, + and now you can fill the hole `{ }` - navigate to the hole `{ }` using `C-c C-f` (forward) or `C-c C-b` (backward) - - press `C-c C-r` and agda will try to help you (r for refine) + - enter `C-c C-r` and agda will try to help you (`r` stands for _refine_) - you should see `λ x → { }` - navigate to the new hole - - `C-c C-,` to check the goal (`C-c C-comma`) - - the Goal area should look like + - enter `C-c C-,` to check the _goal_ (`C-c C-comma`) + - the Goal area ('agda information' window) should look like ```agda Goal: ⊤ @@ -56,10 +56,12 @@ TrueToTrue = {!!} ``` - you have a proof/recipe/generalized element `x : ⊤` - and you need to give a p/r/g.e. of `⊤` - - you can give it a p/r/g.e. of `⊤` and press `C-c C-SPC` to fill the hole + and you need to give a proof/recipe/generalized element of `⊤` + - you can give it a proof/recipe/generalized element of `⊤` + and press `C-c C-SPC` to fill the hole (`SPC` means the space button) -There is more than one proof (see solutions) - are they 'the same'? +There is more than one proof (see solutions) - +are they 'the same'? What is 'the same'? Here is an important solution: @@ -72,7 +74,10 @@ TrueToTrue' x = {!!} - Naviagate to the hole and check the goal. - Note `x` is already taken out for you. - You can try type `x` in the hole and `C-c C-c` - - `c` stands for 'cases on `x`' and the only case is `tt`. + - `c` stands for 'cases'. + Doing `C-c C-c` with `x` in the hole + tells agda to 'do cases on `x`'. + The only case is `tt`. Built into the definition of `⊤` is agda's way of making a map out of ⊤ into another type A, which we have just used. @@ -107,7 +112,9 @@ explosion x = {!!} Agda knows that there are no cases so there is nothing to do! This has three interpretations: - false implies anything (principle of explosion) - - ? + - One can convert recipes of `⊥` to recipes of + any other construction since + there are no recipes of `⊥`. - `⊥` is initial in the category `Type` We can also encode "natural numbers" as a type. @@ -118,14 +125,13 @@ data ℕ : Type where suc : ℕ → ℕ ``` -As a construction, this reads ' +As a construction, this reads : - `ℕ` is a type of construction - `zero` is a recipe for `ℕ` - `suc` takes an existing recipe for `ℕ` and gives another recipe for `ℕ`. - ' -We can see `ℕ` categorically : +We can also see `ℕ` categorically : ℕ is a natural numbers object in the category `Type`. This means it is equipped with morphisms `zero : ⊤ → ℕ` and `suc : ℕ → ℕ` such that @@ -136,7 +142,7 @@ such that the diagram commutes: width="500" class="center"/> -This has no interpretation as a proposition since +`ℕ` has no interpretation as a proposition since there are 'too many proofs' - mathematicians classically don't distinguish between proofs of a single proposition. @@ -151,16 +157,19 @@ go to Quest1! You may have noticed the notational similarities between `zero : ℕ` and `ℕ : Type`. This may have lead you to the question, `Type : ?`. -In type theory, we simply assert `Type : Type 1`. -But then we are chasing our tail, asking `Type 1 : ?`. -Type theorists make sure that every type (the thing on the right side of the `:`) -itself is a term, and every term has a type. +In type theory, we simply assert `Type : Type₁`. +But then we are chasing our tail, asking `Type₁ : Type₂`. +Type theorists make sure that every type +(i.e. anything the right side of `:`) +itself is a term (i.e. anything on the left of `:`), +and every term has a type. So what we really need is ``` Type : Type₁, Type₁ : Type₂, Type₂ : Type₃, ⋯ ``` These are called _universes_. The numberings of universes are called _levels_. +We will start using universes in the next quest. diff --git a/Trinitarianism/Quest2.md b/Trinitarianism/Quest2.md index 728d49a..2ac137c 100644 --- a/Trinitarianism/Quest2.md +++ b/Trinitarianism/Quest2.md @@ -3,8 +3,8 @@ We will try to formulate and prove the statement > The sum of two even naturals is even. To do so we must define `+` on the naturals. -Addition takes in two naturals and spits out a -natural, so it should have type `ℕ → ℕ → ℕ`. +Addition takes in two naturals and spits out a natural, +so it should have type `ℕ → ℕ → ℕ`. ```agda _+_ : ℕ → ℕ → ℕ n + m = ? @@ -12,8 +12,8 @@ n + m = ? Agda supports the notation `_+_` (without spaces) which means from now on you can write `0 + 1` and so on (with spaces). -Try coming up with a sensible definition yourself, -it may not look exactly like ours. +Try coming up with a sensible definition. +It may not look 'the same' as ours.
Hint `n + 0` should be `n` and `n + (m + 1)` should be `(n + m) + 1` @@ -38,27 +38,30 @@ There are three ways to interpret this: - `isEven (_ .fst + _ .fst)` is a bundle over the categorical product `Σ ℕ isEven × Σ ℕ isEven` and `SumOfEven` is a _section_ of the bundle. -More generally given `A : Type` and `B : A → Type` we can form the _pi type_ -`(x : A) → B x : Type` (in other languages `Π (x : ℕ), isEven n`). +More generally given `A : Type` and `B : A → Type` +we can form the _pi type_ `(x : A) → B x : Type` +(in other languages `Π (x : ℕ), isEven n`). The notation suggests that these behave like functions, and indeed in the special case where the fiber is constant -with respect to the base a section is just a term of type `A → B`, -i.e. a function. Hence pi types are also known as -_dependent function types_. +with respect to the base space +a section is just a term of type `A → B`, i.e. a function. +Hence pi types are also known as _dependent function types_. We are now in a position to prove the statement. Have fun! _Important_: Once you have proven the statement, check out our two ways of defining addition `_+_` and `_+'_` (in the solutions). -Use `C-c C-n` to check that they compute the same values -on different examples. -Uncomment the code for `Sum'OfEven` in the solutions, -it is just `SumOfEven` but with `+`s changed for `+'`s. -Load the file. Does the proof still work? +- Use `C-c C-n` to check that they compute the same values + on different examples. +- Uncomment the code for `Sum'OfEven` in the solutions. + It is just `SumOfEven` but with `+`s changed for `+'`s. +- Load the file. Does the proof still work? -In our proof of `SumOfEven` we explicitely used the definition of `_+_`, -which means that if we wanted to use our proof on someone else's -definition of addition, things might break. +Our proof `SumOfEven` relied on +the explicit definition of `_+_`, +which means if we wanted to use our proof on +someone else's definition of addition, +it might not work anymore. > But `_+_` and `_+'_` compute the same values. > Are `_+_` and `_+'_` 'the same'? What is 'the same'? diff --git a/Trinitarianism/README.md b/Trinitarianism/README.md index 9d5dc9a..85e12c8 100644 --- a/Trinitarianism/README.md +++ b/Trinitarianism/README.md @@ -1,7 +1,7 @@ Trinitarianism ============== -By the end of this arc we will have 'a place to do maths'. +By the end of this arc we will (almost) have 'a place to do maths'. The 'types' that will populated this 'place' will have three interpretations: - Proof theoretically, with types as propositions @@ -16,12 +16,14 @@ will have three interpretations: ## Terms and Types Here are some things that we could like to have in a 'place to do maths' - - objects to reason about (like ℕ) - - recipes for making things inside objects (like + 1) - - propositions to reason with (with the data of proofs) (like _ = 0) + - objects to reason about (E.g. `ℕ`) + - recipes for making things inside objects + (E.g. `n + m` for `n` and `m` in naturals.) + - propositions to reason with (E.g. `n = 0` for `n` in naturals.) In proof theory, types are propositions and terms of a type are their proofs. -In type theory, types are programs and terms are algorithms. +In type theory, types are programs / constructions and +terms are algorithms / recipes. In category theory, types are objects and terms are generalised elements. ## Non-dependent Types @@ -34,10 +36,14 @@ In category theory, types are objects and terms are generalised elements. ## Dependent Types -- predicate / type family / over category -- substitution / substitution / pullback -- existence / Σ type / left adjoint to pullback -- for all / Π type / right adjoint to pullback +- predicate / type family / bundle +- substitution / substitution / pullback (of bundles) +- existence / Σ type / total space of bundles +- for all / Π type / space of sections of bundles +## Something doesn't feel the Same -> Question: how do we talk about equality? +There will be one thing missing from this 'place to do maths' +and that is a notion of _equality_. +This is where HoTT deviates from its predecessors, +and is the theme of the next arc. diff --git a/_build/2.6.3/agda/Trinitarianism/Preambles/P1.agdai b/_build/2.6.3/agda/Trinitarianism/Preambles/P1.agdai new file mode 100644 index 0000000..9e73d6c Binary files /dev/null and b/_build/2.6.3/agda/Trinitarianism/Preambles/P1.agdai differ diff --git a/_build/2.6.3/agda/Trinitarianism/Preambles/P2.agdai b/_build/2.6.3/agda/Trinitarianism/Preambles/P2.agdai new file mode 100644 index 0000000..23d5416 Binary files /dev/null and b/_build/2.6.3/agda/Trinitarianism/Preambles/P2.agdai differ diff --git a/_build/2.6.3/agda/Trinitarianism/Quest1Solutions.agdai b/_build/2.6.3/agda/Trinitarianism/Quest1Solutions.agdai new file mode 100644 index 0000000..f29337d Binary files /dev/null and b/_build/2.6.3/agda/Trinitarianism/Quest1Solutions.agdai differ diff --git a/_build/2.6.3/agda/Trinitarianism/Quest2Solutions.agdai b/_build/2.6.3/agda/Trinitarianism/Quest2Solutions.agdai new file mode 100644 index 0000000..79e4dd0 Binary files /dev/null and b/_build/2.6.3/agda/Trinitarianism/Quest2Solutions.agdai differ