Quest1 start

Trinitarianism/AsCats.agda

@@ -1,15 +0,0 @@
-module Trinitarianism.AsCats where
-
-{-
-  Here are some things that we could like to have in a category
-  (in which we want to do maths e.g. the category of sets)
-  * Initial objects (empty set)
-  * Terminal objects (singleton)
-  * Sums
-  * Products
-  * Cartesian closed (for two objects A B, maps A → B
-    are also an object in the category)
-  * Natural numbers object (the natural numbers ℕ in Set)
-  * and maybe more
-
--}

Trinitarianism/Quest0.agda

@@ -1,11 +1,7 @@
 module Trinitarianism.Quest0 where
 open import Trinitarianism.Quest0Preamble
 
-private
-  postulate
-    u : Level
-
-data ⊤ : Type u where
+data ⊤ : Type where
   trivial : ⊤
 
 TrueToTrue : ⊤ → ⊤
@@ -14,11 +10,11 @@ TrueToTrue = {!!}
 TrueToTrue' : ⊤ → ⊤
 TrueToTrue' x = {!!}
 
-data ⊥ : Type u where
+data ⊥ : Type where
 
 explosion : ⊥ → ⊤
 explosion x = {!!}
 
-data ℕ : Type u where
+data ℕ : Type where
   zero : ℕ
   suc : ℕ → ℕ

Trinitarianism/Quest0.md

@@ -1,24 +1,22 @@
-There are three ways of looking at `A : Type u`.
+# Terms and Types
+
+There are three ways of looking at `A : Type`.
   - proof theoretically, '`A` is a proposition'
   - type theoretically, '`A` is a construction'
-  - categorically, '`A` is an object in category `Type u`'
-
-We will explain what u : Level and Type u is at the end of Quest1.
+  - 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
   - the proposition '`A` implies `B`'
   - the construction 'ways to convert `A` recipes to `B` recipes'
-  - internal hom of the category `Type u`
+  - internal hom of the category `Type`
 
 To give examples of this, let's make some types first!
 
 ```agda 
-
 -- Here is how we define 'true'
 data ⊤ : Type u where
   trivial : ⊤
-
 ```
 
 It reads '`⊤` is an inductive type with a constructor `trivial`',
@@ -27,6 +25,8 @@ 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 `⊤`:
 
@@ -44,7 +44,7 @@ TrueToTrue = {!!}
   - `C-c C-,` to check the goal (`C-c C-comma`)
   - the Goal area should look like
 
-  ```
+  ```agda
   Goal: ⊤
   —————————————————————————
   x : ⊤
@@ -58,10 +58,8 @@ There is more than one proof (see solutions) - are they the same?
 Here is an important one:
 
 ```agda
-
-TrueToTrue' : ⊤ → ⊤
-TrueToTrue' x = {!!}
-
+TrueToTrue : ⊤ → ⊤
+TrueToTrue x = {!!}
 ```
 
 
@@ -123,15 +121,15 @@ As a construction, this reads '
   '
 
 We can see `ℕ` as a categorical notion:
-ℕ is a natural numbers object in the category `Type u`,
+ℕ is a natural numbers object in the category `Type`,
 with `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"/>
 
 This has no interpretation as a proposition since
-there are too many terms,
-since mathematicians classically didn't distinguish
+there are 'too many terms/proofs' -
+mathematicians classically didn't distinguish
 between proofs of the same thing.
 (ZFC doesn't even mention logic internally,
 unlike Type Theory!)
@@ -139,4 +137,19 @@ unlike Type Theory!)
 To see how to use terms of type `ℕ`, i.e. induct 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 : ?`.
+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, ⋯ 
+```
+These are called _universes_.
+We will see definitions, for example _groups_
+that will require multiple universes.

Trinitarianism/Quest0Solutions.agda

@@ -1,11 +1,8 @@
 module Trinitarianism.Quest0Solutions where
 open import Trinitarianism.Quest0Preamble
 
-private
-  postulate
-    u : Level
 
-data ⊤ : Type u where
+data ⊤ : Type where
   trivial : ⊤
 
 TrueToTrue : ⊤ → ⊤
@@ -20,11 +17,11 @@ TrueToTrue'' trivial = trivial
 TrueToTrue''' : ⊤ → ⊤
 TrueToTrue''' x = trivial
 
-data ⊥ : Type u where
+data ⊥ : Type where
 
 explosion : ⊥ → ⊤
-explosion x = {!!}
+explosion ()
 
-data ℕ : Type u where
+data ℕ : Type where
   zero : ℕ
   suc : ℕ → ℕ

Trinitarianism/Quest1.agda

@@ -0,0 +1,9 @@
+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

Trinitarianism/Quest1.md

@@ -0,0 +1,14 @@
+# Dependent Types
+
+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
+
+```agda
+isEven : ℕ → Type u
+isEven n = ? 
+```

Trinitarianism/README.md

@@ -2,7 +2,7 @@
 Trinitarianism
 ==============
 By the end of this arc we will have 'a place to do maths'. 
-The following features will have three interpretations:
+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