diff --git a/Trinitarianism/AsCats.agda b/Trinitarianism/AsCats.agda deleted file mode 100644 index 92f7ac6..0000000 --- a/Trinitarianism/AsCats.agda +++ /dev/null @@ -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 - --} diff --git a/Trinitarianism/Quest0.agda b/Trinitarianism/Quest0.agda index 31607c0..41956fa 100644 --- a/Trinitarianism/Quest0.agda +++ b/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 : ℕ → ℕ diff --git a/Trinitarianism/Quest0.md b/Trinitarianism/Quest0.md index 7765f32..f688f32 100644 --- a/Trinitarianism/Quest0.md +++ b/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: nno 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. diff --git a/Trinitarianism/Quest0Solutions.agda b/Trinitarianism/Quest0Solutions.agda index 51331f8..b1e7dc3 100644 --- a/Trinitarianism/Quest0Solutions.agda +++ b/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 : ℕ → ℕ diff --git a/Trinitarianism/Quest1.agda b/Trinitarianism/Quest1.agda new file mode 100644 index 0000000..709a30a --- /dev/null +++ b/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 diff --git a/Trinitarianism/Quest1.md b/Trinitarianism/Quest1.md new file mode 100644 index 0000000..2654930 --- /dev/null +++ b/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 = ? +``` diff --git a/Trinitarianism/README.md b/Trinitarianism/README.md index d1487f7..7ee9b6e 100644 --- a/Trinitarianism/README.md +++ b/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 diff --git a/_build/2.6.2/agda/Trinitarianism/AsCats.agdai b/_build/2.6.2/agda/Trinitarianism/AsCats.agdai index ab957bf..c576fe7 100644 Binary files a/_build/2.6.2/agda/Trinitarianism/AsCats.agdai and b/_build/2.6.2/agda/Trinitarianism/AsCats.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/Quest0Preamble.agdai b/_build/2.6.2/agda/Trinitarianism/Quest0Preamble.agdai index 127e079..efab688 100644 Binary files a/_build/2.6.2/agda/Trinitarianism/Quest0Preamble.agdai and b/_build/2.6.2/agda/Trinitarianism/Quest0Preamble.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai b/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai new file mode 100644 index 0000000..816ddff Binary files /dev/null and b/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai differ