diff --git a/Trinitarianism/Quest0.md b/Trinitarianism/Quest0.md index f688f32..4c04f41 100644 --- a/Trinitarianism/Quest0.md +++ b/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: -nno +nno 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_. + + diff --git a/Trinitarianism/Quest1.agda b/Trinitarianism/Quest1.agda index 709a30a..424f045 100644 --- a/Trinitarianism/Quest1.agda +++ b/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 = {!!} + diff --git a/Trinitarianism/Quest1.md b/Trinitarianism/Quest1.md index 2654930..1bccdf1 100644 --- a/Trinitarianism/Quest1.md +++ b/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). diff --git a/Trinitarianism/README.md b/Trinitarianism/README.md index 7ee9b6e..9d5dc9a 100644 --- a/Trinitarianism/README.md +++ b/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 - - +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 +the holy trinity + ## Terms and Types Here are some things that we could like to have in a 'place to do maths' diff --git a/Trinitarianism/images/trinitarianism.png b/Trinitarianism/images/trinitarianism.png new file mode 100644 index 0000000..0adef44 Binary files /dev/null and b/Trinitarianism/images/trinitarianism.png differ diff --git a/_build/2.6.3/agda/Trinitarianism/Quest0Solutions.agdai b/_build/2.6.3/agda/Trinitarianism/Quest0Solutions.agdai index c2ae7f3..98651e8 100644 Binary files a/_build/2.6.3/agda/Trinitarianism/Quest0Solutions.agdai and b/_build/2.6.3/agda/Trinitarianism/Quest0Solutions.agdai differ diff --git a/_build/2.6.3/agda/Trinitarianism/Quest1.agdai b/_build/2.6.3/agda/Trinitarianism/Quest1.agdai new file mode 100644 index 0000000..1bfb08d Binary files /dev/null and b/_build/2.6.3/agda/Trinitarianism/Quest1.agdai differ