diff --git a/Trinitarianism/Quest0.agda b/Trinitarianism/Quest0.agda index 39c894e..dcb28cd 100644 --- a/Trinitarianism/Quest0.agda +++ b/Trinitarianism/Quest0.agda @@ -1,324 +1,23 @@ module Trinitarianism.Quest0 where open import Trinitarianism.Quest0Preamble -private - postulate - u : Level +postulate + u : Level - -{- -There are three ways of looking at `A : Type u`. - - 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. - -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` - -To give examples of this, let's make some types first! --} - --- Here is how we define 'true' data ⊤ : Type u where trivial : ⊤ -{- - -It reads '`⊤` is an inductive type with a constructor `trivial`', -with three interpretations - - `⊤` is a proposition and there is a proof of it, called `trivial`. - - `⊤` is a construction with a recipe called `trivial` - - `⊤` is a terminal object: every object has a morphism into `⊤` given by `· ↦ trivial` - -The above tells you how we _make_ a term of type `⊤`, -let's see an example of _using_ a term of type `⊤`: --} - TrueToTrue : ⊤ → ⊤ TrueToTrue = {!!} -{- - - press `C-c C-l` (this means `Ctrl-c Ctrl-l`) to load the document, - and now you can fill the holes - - 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) - - 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 - - ``` - Goal: ⊤ - ————————————————————————— - x : ⊤ - ``` - - - 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 - -There is more than one proof (see solutions) - are they the same? -Here is an important one: --} 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` - - `c` stands for 'cases on `x`' and the only case is `trivial`. - -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 - - the only proof of `⊤` is `trivial` - - the only recipe for `⊤` is `trivial` - - the only one generalized element `trivial` in `⊤` --} - - - --- 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 - - `⊥` is a construction with no recipes - - There are no generalized elements of `⊥` (it is a strict initial object) - -Let's try mapping out of `⊥`. --} - explosion : ⊥ → ⊤ explosion x = {!!} -{- - - - Navigate to the hole and do cases on `x`. - -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` - --} - -{- -We can also encode "natural numbers" as a type. --} -data ℕ : Type where +data ℕ : Type u where zero : ℕ suc : ℕ → ℕ -{- -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 `ℕ` as a categorical notion: -ℕ is a natural numbers object in the category `Type u`, -with `zero : ⊤ → ℕ` and `suc : ℕ → ℕ` such that -given any `⊤ → A → A` there exist a unique morphism `ℕ → A` -such that the diagram commutes: - - -This has no interpretation as a proposition since -there are too many terms, -since mathematicians classically didn't distinguish -between proofs of the same thing. -(ZFC doesn't even mention logic internally, -unlike Type Theory!) - - - - --} - -postulate - A : Type u - -NNO : A → (A → A) → (ℕ → A) -NNO a s zero = a -NNO a s (suc n) = s (NNO a s n) - - - - - - - - - - - - - - - -{- -Let's assume we have the following the naturals ℕ -and try to define the 'predicate on ℕ' given by 'x is 0' --} -isZero : ℕ → Type u -isZero zero = {!!} -isZero (suc n) = {!!} - -{- -Here's how: - * when x is zero, we give the proposition ⊤ - (try typing it in by writing \top then pressing C-c C-SPC) - * when x is suc n (i.e. 'n + 1', suc for successor) we give ⊥ (\bot) -This is technically using induction - see AsTypes. - -In general a 'predicate on ℕ' is just a 'function' P : ℕ → Type u --} - -{- -You can check if zero is indeed zero by clicking C-c C-n, -which brings up a thing on the bottom saying 'Expression', -and you can type the following -isZero zero -isZero (suc zero) -isZero (suc (suc zero)) -... --} - -{- -We can prove that 'there exists a natural number that isZero' -in set theory we might write - ∃ x ∈ ℕ, x = 0 -which in agda noation is - Σ ℕ isZero - -In general if we have predicate P : ℕ → Type u we would write - Σ ℕ P -for - ∃ x ∈ ℕ, P x - -To formulate the result Σ ℕ isZero we need to define -a proof of it --} -ExistsZero : Σ ℕ isZero -ExistsZero = {!!} - -{- -To fill the hole, we need to give a natural and a proof that it is zero. -Agda will give the syntax you need: - * navigate to the correct hole then refine using C-c C-r - * there are now two holes - but which is which? - * navigate to the first holes and type C-c C-, - - for the first hole it will ask you to give it a natural 'Goal: ℕ' - - for the second hole it will ask you for a proof that - whatever you put in the first hole is zero 'Goal: isZero ?0' for example - * try to fill both holes, using C-c C-SPC as before - * for the second hole you can try also C-c C-r, - Agda knows there is an obvious proof! --} - -{- -Let's show 'if all natural numbers are zero then we have a contradiction', -where 'a contradiction' is a proof of ⊥. -In maths we would write - (∀ x ∈ ℕ, x = 0) → ⊥ -and the agda notation for this is - ((x : ℕ) → isZero x) → ⊥ - -In general if we have a predicate P : ℕ → Prop then we write - (x : ℕ) → P x -to mean - ∀ x ∈ ℕ, P x --} - -AllZero→⊥ : ((x : ℕ) → isZero x) → ⊥ -AllZero→⊥ = {!!} - -{- -Here is how we prove it in maths - * assume hypothesis h, a proof of (x : ℕ) → isZero x - * apply the hypothesis h to 1, deducing isZero 1, i.e. we get a proof of isZero 1 - * notice isZero 1 IS ⊥ - -Here is how you can prove it here - * navigate to the hole and check the goal - * to assume the hypothesis (x : ℕ) → isZero x, - type an h in front like so - AllZero→⊥ h = { } - * now do - * C-c C-l to load the file - * navigate to the new hole and check the new goal - * type h in the hole, type C-c C-r - * this should give h { } - * navigate to the new hole and check the Goal - * Explanation - * (h x) is a proof of isZero x for each x - * it's now asking for a natural x such that isZero x is ⊥ - * Try filling the hole with 0 and 1 and see what Agda says --} - -{- -Let's try to show the mathematical statement -'any natural n is 0 or not' -but we need a definition of 'or' --} -data OR (P Q : Type u) : Type u where - left : P → OR P Q - right : Q → OR P Q -{- -This reads - * Given propositions P and Q we have another proposition P or Q - * There are two ways of proving P or Q - * given a proof of P, left sends this to a proof of P or Q - * given a proof of Q, right sends this to a proof of P or Q - -Agda supports nice notation using underscores. --} - -data _∨_ (P Q : Type u) : Type u where - left : P → P ∨ Q - right : Q → P ∨ Q - -{- -[Important note] -Agda is sensitive to spaces so these are bad - -data _ ∨ _ (P Q : Prop) : Prop where - left : P → P ∨ Q - right : Q → P ∨ Q - -data _∨_ (P Q : Prop) : Prop where - left : P → P∨Q - right : Q → P∨Q - -it is also sensitive to indentation so these are also bad - -data _∨_ (P Q : Prop) : Prop where -left : P → P ∨ Q -right : Q → P ∨ Q - --} - -{- -Now we can prove it! -This technically uses induction - see AsTypes. -Fill the missing part of the theorem statement. -You need to first uncomment this by getting rid of the -- in front (C-x C-;) --} --- DecidableIsZero : (n : ℕ) → {!!} --- DecidableIsZero zero = {!!} --- DecidableIsZero (suc n) = {!!} - --- TODO terms and types --- TODO universe levels diff --git a/Trinitarianism/Quest0.md b/Trinitarianism/Quest0.md index 74cdba6..7765f32 100644 --- a/Trinitarianism/Quest0.md +++ b/Trinitarianism/Quest0.md @@ -3,7 +3,7 @@ There are three ways of looking at `A : Type u`. - 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. +We will explain what u : Level and Type u is at the end of Quest1. 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 diff --git a/Trinitarianism/Quest0Preamble.agda b/Trinitarianism/Quest0Preamble.agda index d5564dd..95c03ec 100644 --- a/Trinitarianism/Quest0Preamble.agda +++ b/Trinitarianism/Quest0Preamble.agda @@ -1,4 +1,3 @@ - module Trinitarianism.Quest0Preamble where open import Cubical.Core.Everything hiding (_∨_) public diff --git a/_build/2.6.3/agda/Trinitarianism/Quest0Preamble.agdai b/_build/2.6.3/agda/Trinitarianism/Quest0Preamble.agdai new file mode 100644 index 0000000..6a29d8d Binary files /dev/null and b/_build/2.6.3/agda/Trinitarianism/Quest0Preamble.agdai differ