Checked Trinitarianism.

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
+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. 

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.
 
 <!--
 Everything we will make will be closed in 

Trinitarianism/Quest1.agda

@@ -5,5 +5,11 @@ open import Trinitarianism.Preambles.P1
 isEven : ℕ → Type
 isEven n = {!!}
 
+{-
+This is a comment block.
+Remove this comment block and formulate
+'there exists an even natural' here.
+-}
+
 div2 : Σ ℕ isEven → ℕ
 div2 x = {!!}

Trinitarianism/Quest1.md

@@ -33,7 +33,7 @@ isEven n = ?
   `zero` and `suc n`, 
   since these are the only constructors given 
   in the definition of `ℕ`."
-  This has the following interpretations,
+  This has the following interpretations :
   - propositionally, this is the _principle of mathematical induction_.
   - categorically, this is the universal property of a
     natural numbers object.
@@ -74,17 +74,16 @@ isEven n = ?
   The reason we have access to the term `isEven n` is again
   because we are in the 'inductive step'.
 - There should now be nothing in the 'agda info' window.
-  Everything is working!
+  This means everything is working.
 
 There are three interpretations of `isEven : ℕ → Type`.
 - Already mentioned, `isEven` is a predicate on `ℕ`.
 - `isEven` is a _dependent construction_.
-  Specifically, it is either `⊤` or `⊥` depending on `n : ℕ`.
+  Specifically, `isEven n` is either `⊤` or `⊥` depending on `n : ℕ`.
 - `isEven` is a _bundle over `ℕ`_,
   i.e. an object in the over-category `Type↓ℕ`.
   Pictorially, it looks like
   
-
   <img src="images/isEven.png" 
      alt="isEven" 
      width="500"/>
@@ -97,7 +96,7 @@ There are three interpretations of `isEven : ℕ → Type`.
 In general given a type `A : Type`, 
 a _dependent type over `A`_ is a term of type `A → Type`.
  
-You can check if `2` is even by asking agda to 'normalize' it:
+You can check if `2` is even by asking agda to 'reduce' the term `isEven 2`:
 do `C-c C-n` (`n` for normalize) and type in `isEven 2`.
 (By the way you can write in numerals since we are now secretly 
 using `ℕ` from the cubical agda library.)
@@ -105,24 +104,25 @@ using `ℕ` from the cubical agda library.)
 Now that we have expressed `isEven` we need to be able write down "existence".
 In maths we might write 
 ```∃ x ∈ ℕ, isEven x```
-which in Agda notation is 
+which in agda notation is 
 ```Σ ℕ isEven```
 This is called a _sigma type_, which has three interpretations:
 - the proposition 'there exists an even natural'
-- the constructions 'naturals `n` with recipes of `isEven n`'
+- the construction 
+  'keep a recipe `n` of naturals together with a recipe of `isEven n`'
 - the total space of the bundle `isEven` over `ℕ`,
-  which is the space consisting of the all the fibers.
+  which is the space obtained by putting together all the fibers.
   Pictorially, it looks like
   <img src="images/isEvenBundle.png" 
      alt="SigmaTypeOfIsEven" 
      width="500"/>
   which can also be viewed as the subset of even naturals,
-  since the fibers are either empty or singleton 
-  (it is a _subsingleton bundle_).
+  since the fibers are either empty or singleton. 
+  (It is a _subsingleton bundle_).
 
 Making a term of this type has three interpretations:
-- giving a term `n : ℕ` and a proof `hn : isEven n` that `n` is even.
-- constructing a natural `n : ℕ` and a recipe `hn : isEven n`.
+- a natural `n : ℕ` together with a proof `hn : isEven n` that `n` is even.
+- a recipe `n : ℕ` together with a recipe `hn : isEven n`.
 - a point in the total space is a point `n : ℕ` downstairs
   together with a point `hn : isEven n` in its fiber.
 
@@ -135,11 +135,11 @@ Name = ?
 - Load the file, go to the hole and refine the goal.
 - If you formulated the statement right it should split into `{!!} , {!!}`
   and you can check the types of terms the holes require.
-- Fill the holes, there are many proofs you can do!
+- Fill the holes. There are many proofs you can do!
 
 In general when `A : Type` is a type and `B : A → Type` is a 
 predicate/dependent construction/bundle over `A`, 
-we can write `Σ A B` as the collection of pairs `a , b` 
+we can write the type `Σ A B` whose terms are pairs `a , b` 
 where `a : A` and `b : B a`.
 
 There are two ways of using a term in a sigma type.
@@ -147,7 +147,7 @@ We can extract the first part using `fst` or the second part using `snd`.
 Given `x : Σ A B` there are three interpretations of `fst` and `snd`:
 - Viewing `x` as a proof of existence
   `fst x` provides the witness of existence and `snd` provides the proof 
-  of the property
+  that the witness `fst x` has the desired property
 - Viewing `x` as a recipe `fst` extracts the first component and 
   `snd` extracts the second component 
 - Viewing `x` as a point in the total space of a bundle 
@@ -156,37 +156,45 @@ Given `x : Σ A B` there are three interpretations of `fst` and `snd`:
   In particular you can interpret `fst` as projection from the total space
   to the base space, collapsing fibers.
 For example to define a map that takes an even natural and divides it by two 
-we can 
+we can do 
 ```agda
 div2 : Σ ℕ isEven → ℕ
 div2 x = ? 
 ```
-- Load the file, go to the hole and case on `x` 
-  (you might want to rename `fst₁` and `snd₁`). 
-```agda
-div2 : Σ ℕ isEven → ℕ
-div2 (fst₁ , snd₁) = {!!}
-```
-- Case on `fst₁` and tell it what to give for `0 , _`
-```agda
-div2 : Σ ℕ isEven → ℕ
-div2 (zero , snd₁) = {!!}
-div2 (suc fst₁ , snd₁) = {!!}
-```
+- Load the file, go to the hole and case on `x`.
+  You might want to rename `fst₁` and `snd₁`. 
+  ```agda
+  div2 : Σ ℕ isEven → ℕ
+  div2 (fst₁ , snd₁) = {!!}
+  ```
+- Case on `fst₁` and tell agda what to give for `0 , _`,
+  i.e. what 'zero divided by two' ought to be.
+  ```agda
+  div2 : Σ ℕ isEven → ℕ
+  div2 (zero , snd₁) = {!!}
+  div2 (suc fst₁ , snd₁) = {!!}
+  ```
 - Navigate to the second hole and case on `fst₁` again.
   Notice that agda knows there is no term looking like `1 , _`
   so it has skipped that case for us.
-- `n + 2 / 2` should just be `n/2 + 1` so try writing in `suc` and refining the goal
+  ```agda
+  div2 : Σ ℕ isEven → ℕ
+  div2 (zero , snd₁) = 0
+  div2 (suc (suc fst₁) , snd₁) = {!!}
+  ```
+- `(n + 2) / 2` should just be `n/2 + 1` 
+  so try writing in `suc` and refining the goal
 - How do you write down `n/2`? Hint: we are in the 'inductive step'.
 
 Try dividing some terms by `2`:
 - Use `C-c C-n` and write `div2 (2 , tt)` for example.
 - Try dividing `36` by `2`.
 
-Important observation: the two proofs `2 , tt` and `36 , tt` of the statement 
+*Important Observation* : 
+the two proofs `2 , tt` and `36 , tt` of the statement 
 'there exists an even natural' are not 'the same' in any sense,
 since if they were `div2 (2 , tt)` would be 'the same' `div2 (36/2 , tt)`,
-hence `1` would be 'the same' as `18`. 
+and hence `1` would be 'the same' as `18`. 
 > Are they 'the same'? What is 'the same'? 
 <!-- see Arc/Quest smth? -->
 

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.
 <details>
   <summary>Hint</summary>
   `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'?

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.