Continued isEven.

Trinitarianism/Quest0.md

@@ -6,7 +6,8 @@ There are three ways of looking at `A : Type`.
   - categorically, '`A` is an object in category `Type`'
 
 A first example of a type construction is the function type.
-Given types `A` and `B`, we have another type `A → B` which can be seen as
+Given types `A : Type` and `B : Type`, 
+we have another type `A → B : Type` which can be seen as
   - the proposition '`A` implies `B`'
   - the construction 'ways to convert `A` recipes to `B` recipes'
   - internal hom of the category `Type`
@@ -25,10 +26,14 @@ with three interpretations
   - `⊤` is a construction with a recipe called `trivial`
   - `⊤` is a terminal object: every object has a morphism into `⊤` given by `· ↦ trivial`
 
-What goes on the right of the `:` is called a type, and will always be in (some) `Type`,
-and what goes on the left is called a term of that term.
-The above tells you how we _make_ a term of type `⊤`,
-let's see an example of _using_ a term of type `⊤`:
+In general, the expression `a : A` is read '`a` is a term of type `A`',
+and has three interpretations,
+  - `a` is a proof of the proposition `A`
+  - `a` is a recipe for the construction `A`
+  - `a` is a generalised element of the object `A` in the category `Type`.
+
+The above tells you how we _make_ a term of type `⊤`.
+Let's see an example of _using_ a term of type `⊤`:
 
 ```agda
 TrueToTrue : ⊤ → ⊤
@@ -58,11 +63,10 @@ There is more than one proof (see solutions) - are they the same?
 Here is an important one:
 
 ```agda
-TrueToTrue : ⊤ → ⊤
-TrueToTrue x = {!!}
+TrueToTrue' : ⊤ → ⊤
+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`
@@ -70,19 +74,19 @@ TrueToTrue x = {!!}
 
 Built into the definition of `⊤` is agda's way of making a map out of ⊤
 into another type A, which we have just used.
-It says to map out of ⊤ it suffices to do the case when `x` is `trivial`, or
+It says 'to map out of ⊤ it suffices to do the case when `x` is `trivial`', or
   - the only proof of `⊤` is `trivial`
   - the only recipe for `⊤` is `trivial`
   - the only one generalized element `trivial` in `⊤`
 
+Let's define another type.
+
 ```agda
 
--- Here is how we define 'false'
 data ⊥ : Type u where
 
 ```
 
-
 It reads '`⊥` is an inductive type with no constructors',
 with three interepretations
   - `⊥` is a proposition with no proofs
@@ -102,8 +106,7 @@ Agda knows that there are no cases so there is nothing to do!
 This has three interpretations:
   - false implies anything (principle of explosion)
   - ?
-  - `⊥` is initial in the category `Type u`
-
+  - `⊥` is initial in the category `Type`
 
 We can also encode "natural numbers" as a type.
 
@@ -120,36 +123,57 @@ As a construction, this reads '
       another recipe for `ℕ`.
   '
 
-We can see `ℕ` as a categorical notion:
-ℕ is a natural numbers object in the category `Type`,
-with `zero : ⊤ → ℕ` and `suc : ℕ → ℕ` such that
+We can see `ℕ` as categorically :
+ℕ is a natural numbers object in the category `Type`.
+This means it is equipped with morphisms `zero : ⊤ → ℕ` 
+and `suc : ℕ → ℕ` such that
 given any `⊤ → A → A` there exist a unique morphism `ℕ → A`
 such that the diagram commutes:
-<img src="images/nno.png" alt="nno" width="400"/>
+<img src="images/nno.png" 
+     alt="nno" 
+     width="500"
+     class="center"/>
 
 This has no interpretation as a proposition since
-there are 'too many terms/proofs' -
-mathematicians classically didn't distinguish
-between proofs of the same thing.
+there are 'too many proofs' -
+mathematicians classically don't distinguish
+between proofs of a single proposition.
 (ZFC doesn't even mention logic internally,
 unlike Type Theory!)
 
-To see how to use terms of type `ℕ`, i.e. induct on `ℕ`, 
+To see how to use terms of type `ℕ`, i.e. induction on `ℕ`, 
 go to Quest1!
 
 ## Universes
 
 You may have noticed the notational similarities between 
 `zero : ℕ` and `ℕ : Type`.
-Which may lead to the question `Type : ?`.
-We simply assert `Type : Type 1`,
-but then we are chasing our tail, asking `Type 1 : ?`.
+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.
 So what we really need is 
 ```
-Type : Type 1, Type 1 : Type 2, Type 2 : Type 3, ⋯ 
+Type : Type₁, Type₁ : Type₂, Type₂ : Type₃, ⋯
 ```
 These are called _universes_.
-We will see definitions, for example _groups_
-that will require multiple universes.
+The numberings of universes are called _levels_.
+
+<!--
+Everything we will make will be closed in 
+the universe we are in.
+For example,
+
+- Do `C-c C-d`. 
+  Agda will ask you to input an expression.
+- Input `⊤ → ℕ` and hit return.
+
+In the 'agda information' window, you should see `Type`.
+This means Agda has _deduced_ `⊤ → ℕ : Type`.
+In general, you can use `C-c C-d` to check
+the type of terms. 
+
+The reason that `⊤ → ℕ` is a type in `Type`
+is because both `⊤, ℕ` are.
+-->

Trinitarianism/Quest1.agda

@@ -3,7 +3,6 @@ module Trinitarianism.Quest1 where
 open import Cubical.Core.Everything
 open import Trinitarianism.Quest0Solutions
 
-isEven : ℕ → Type u
-isEven zero = ⊤
-isEven (suc zero) = ⊥
-isEven (suc (suc n)) = isEven n
+isEven : ℕ → Type
+isEven zero = {!!}
+

Trinitarianism/Quest1.md

@@ -3,12 +3,86 @@
 In a 'place to do maths'
 we would like to be able to express and 'prove'
 the statement
+
 > There exists a natural that is even.
-This requires the notion of a __predicate_.
-In general a predicate on a type `A` is a term of type 
-`A → Type u`, for example
+
+This requires the notion of a _predicate_.
+In general a predicate on a type `A : Type` is 
+a term of type `A → Type`. 
+For example,
 
 ```agda
-isEven : ℕ → Type u
+isEven : ℕ → Type
 isEven n = ? 
 ```
+
+- Do `C-c C-l` to load the file.
+- Navigate to the hole.
+- Input `n` in the hole and do `C-c C-c`.
+  You should now see 
+  
+  ```agda
+  
+  isEven : ℕ → Type
+  isEven zero = {!!}
+  isEven (suc n) = {!!}
+
+  ```
+  Explanation : 'to define a function on `ℕ`,
+  it suffices to define the function on the __cases_, 
+  `zero` and `suc n`, 
+  since these are the only constructors given 
+  in the definition of `ℕ`'.
+  This has the following interpretations,
+  - propositionally, this is the _principle of mathematical induction_.
+  - categorically, this is the universal property of a
+    natural numbers object.
+- Navigate to the first hole and check the goal.
+  You should see 
+  ```
+  Goal: Type
+  ———————————
+  ```
+  Fill the hole with `⊤`, since we want `zero` to be even.
+- Navigate to the second hole.
+- Input `n` and do `C-c C-c` again.
+  You should now see
+  ```agda
+  isEven : ℕ → Type
+  isEven zero = ⊤
+  isEven (suc zero) = {!!}
+  isEven (suc (suc n)) = {!!} 
+  ```
+  Explanation : 
+  we have just used induction again. 
+- Navigate to the first hole and check the goal.
+  Agda should be asking for a term of type `Type`,
+  so fill the hole with `⊥`,
+  since we don't want `suc zero` to be even.
+- Navigate to the next hole and check the goal.
+  You should see in the 'agda information' window,
+  ```
+  Goal: Type
+  ——————————————
+  n : ℕ
+  ```
+  Explanation :
+  We are in the 'inductive step',
+  so we have access to the previous natural number.
+- Fill the hole with `isEven n`,
+  since we want `suc (suc n)` to be even _precisely when_
+  `n` is even.
+  
+  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!
+
+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 : ℕ`.
+- `isEven` is a _bundle over `ℕ`_,
+  i.e. an object in the over-category `Type↓ℕ`.
+  Pictorially, it looks like (insert picture).

Trinitarianism/README.md

@@ -2,13 +2,17 @@
 Trinitarianism
 ==============
 By the end of this arc we will have 'a place to do maths'. 
-The 'types' that make up this 'place' will have three interpretations:
- - Proof theoretic, with types as propositions
- - Type theoretic, with types as programs
- - Category theoretic, with types as objects in a category
-
-<!-- insert picture of trinitarianism -->
+The 'types' that will populated this 'place' 
+will have three interpretations:
+ - Proof theoretically, with types as propositions
+ - Type theoretically, with types as programs
+ - Category theoretically, with types as objects in a category
 
+<img src="images/trinitarianism.png" 
+     alt="the holy trinity" 
+     width="500"
+     class="center"/>
+ 
 ## Terms and Types
 
 Here are some things that we could like to have in a 'place to do maths'