diff --git a/Trinitarianism/Quest0.agda b/Trinitarianism/Quest0.agda index 41956fa..72b5ce8 100644 --- a/Trinitarianism/Quest0.agda +++ b/Trinitarianism/Quest0.agda @@ -2,7 +2,7 @@ module Trinitarianism.Quest0 where open import Trinitarianism.Quest0Preamble data ⊤ : Type where - trivial : ⊤ + tt : ⊤ TrueToTrue : ⊤ → ⊤ TrueToTrue = {!!} diff --git a/Trinitarianism/Quest0.md b/Trinitarianism/Quest0.md index 4c04f41..375c1b1 100644 --- a/Trinitarianism/Quest0.md +++ b/Trinitarianism/Quest0.md @@ -17,14 +17,14 @@ To give examples of this, let's make some types first! ```agda -- Here is how we define 'true' data ⊤ : Type u where - trivial : ⊤ + tt : ⊤ ``` -It reads '`⊤` is an inductive type with a constructor `trivial`', +It reads '`⊤` is an inductive type with a constructor `tt`', 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` + - `⊤` is a proposition and there is a proof of it, called `tt`. + - `⊤` is a construction with a recipe called `tt` + - `⊤` is a terminal object: every object has a morphism into `⊤` given by `· ↦ tt` In general, the expression `a : A` is read '`a` is a term of type `A`', and has three interpretations, @@ -70,14 +70,14 @@ 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`. + - `c` stands for 'cases on `x`' and the only case is `tt`. 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 `⊤` +It says 'to map out of ⊤ it suffices to do the case when `x` is `tt`', or + - the only proof of `⊤` is `tt` + - the only recipe for `⊤` is `tt` + - the only one generalized element `tt` in `⊤` Let's define another type. @@ -123,7 +123,7 @@ As a construction, this reads ' another recipe for `ℕ`. ' -We can see `ℕ` as categorically : +We can see `ℕ` categorically : ℕ is a natural numbers object in the category `Type`. This means it is equipped with morphisms `zero : ⊤ → ℕ` and `suc : ℕ → ℕ` such that diff --git a/Trinitarianism/Quest0Solutions.agda b/Trinitarianism/Quest0Solutions.agda index b1e7dc3..decb41d 100644 --- a/Trinitarianism/Quest0Solutions.agda +++ b/Trinitarianism/Quest0Solutions.agda @@ -3,7 +3,7 @@ open import Trinitarianism.Quest0Preamble data ⊤ : Type where - trivial : ⊤ + tt : ⊤ TrueToTrue : ⊤ → ⊤ TrueToTrue = λ x → x @@ -12,10 +12,10 @@ TrueToTrue' : ⊤ → ⊤ TrueToTrue' x = x TrueToTrue'' : ⊤ → ⊤ -TrueToTrue'' trivial = trivial +TrueToTrue'' tt = tt TrueToTrue''' : ⊤ → ⊤ -TrueToTrue''' x = trivial +TrueToTrue''' x = tt data ⊥ : Type where diff --git a/Trinitarianism/Quest1.agda b/Trinitarianism/Quest1.agda index 424f045..6f1fa15 100644 --- a/Trinitarianism/Quest1.agda +++ b/Trinitarianism/Quest1.agda @@ -1,8 +1,10 @@ module Trinitarianism.Quest1 where open import Cubical.Core.Everything -open import Trinitarianism.Quest0Solutions +open import Cubical.Data.Nat hiding (isEven) isEven : ℕ → Type -isEven zero = {!!} +isEven n = {!!} +div2 : Σ ℕ isEven → ℕ +div2 x = {!!} diff --git a/Trinitarianism/Quest1.md b/Trinitarianism/Quest1.md index 1bccdf1..f3e1652 100644 --- a/Trinitarianism/Quest1.md +++ b/Trinitarianism/Quest1.md @@ -28,11 +28,11 @@ isEven n = ? isEven (suc n) = {!!} ``` - Explanation : 'to define a function on `ℕ`, - it suffices to define the function on the __cases_, + It says "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 `ℕ`'. + 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 @@ -53,8 +53,7 @@ isEven n = ? isEven (suc zero) = {!!} isEven (suc (suc n)) = {!!} ``` - Explanation : - we have just used induction again. + 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 `⊥`, @@ -66,7 +65,6 @@ isEven n = ? —————————————— n : ℕ ``` - Explanation : We are in the 'inductive step', so we have access to the previous natural number. - Fill the hole with `isEven n`, @@ -79,10 +77,100 @@ isEven n = ? 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). + Pictorially, it looks like + + isEven + + In the categorical perspective, for each `n : ℕ` + `isEven n` is called the _fiber over `n`_. + In this particular example the fibers are either empty + or singleton. + +You can check if `2` is even by asking agda to 'normalize' it: +do `C-c C-n` (`n` for normalize) and type in `isEven 2`. +(By the way you can write in numerals since we are now secretly +using `ℕ` from the cubical agda library.) + +Now that we have expressed `isEven` we need to be able write down "existence". +In maths we might write +```∃ x ∈ ℕ, isEven x``` +which in Agda notation is +```Σ ℕ isEven``` +This is called a _sigma type_, which has three interpretations: +- the proposition 'there exists an even natural' +- the constructions 'naturals `n` with recipes of `isEven n`' +- the total space of the bundle `isEven` over `ℕ`, + which is the space consisting of the all the fibers. + Pictorially, it looks like + SigmaTypeOfIsEven + which can also be viewed as the subset of even naturals, + since the fibers are either empty or singleton + (it is a _subsingleton bundle_). + +Making a term of this type has three interpretations: +- giving a term `n : ℕ` and a proof `hn : isEven n` that `n` is even. +- constructing a natural `n : ℕ` and a recipe `hn : isEven n`. +- a point in the total space is a point `n : ℕ` downstairs + together with a point `hn : isEven n` in its fiber. + +Now you can prove that there exists an even natural: +- Formulate the statement you need. Make sure you have it of the form +```agda +Name : Statement +Name = ? +``` +- Load the file, go to the hole and refine the goal. +- If you formulated the statement right it should split into `{!!} , {!!}` + and you can check the types of terms the holes require. +- Fill the holes, there are many proofs you can do! + +In general when `A : Type` is a type and `B : A → Type` is a +predicate/dependent construction/bundle over `A`, +we can write `Σ A B` as the collection of pairs `a , b` +where `a : A` and `b : B a`. + +There are two ways of using a term in a sigma type. +We can extract the first part using `fst` or the second part using `snd`. +For example to define a map that takes an even natural and divides it by two +we can +```agda +div2 : Σ ℕ isEven → ℕ +div2 x = ? +``` +- Load the file, go to the hole and case on `x` + (you might want to rename `fst₁` and `snd₁`). +```agda +div2 : Σ ℕ isEven → ℕ +div2 (fst₁ , snd₁) = {!!} +``` +- Case on `fst₁` and tell it what to give for `0 , _` +```agda +div2 : Σ ℕ isEven → ℕ +div2 (zero , snd₁) = {!!} +div2 (suc fst₁ , snd₁) = {!!} +``` +- Navigate to the second hole and case on `fst₁` again. + Notice that agda knows there is no term looking like `1 , _` + so it has skipped that case for us. +- `n + 2 / 2` should just be `n/2 + 1` so try writing in `suc` and refining the goal +- How do you write down `n/2`? Hint: we are in the 'inductive step'. + +Try dividing some terms by `2`: +- Use `C-c C-n` and write `div2 (2 , tt)` for example. +- Try dividing `36` by `2`. + +Important observation: the two proofs `2 , tt` and `36 , tt` of the statement +'there exists an even natural' are not 'the same' in any sense, +since if they were `div2 (2 , tt)` would be 'the same' `div2 (36/2 , tt)`, +hence `1` would be 'the same' as `18`. +> Are they 'the same'? What is 'the same'? + diff --git a/Trinitarianism/Quest1Solutions.agda b/Trinitarianism/Quest1Solutions.agda new file mode 100644 index 0000000..74a09dc --- /dev/null +++ b/Trinitarianism/Quest1Solutions.agda @@ -0,0 +1,19 @@ +module Trinitarianism.Quest1Solutions where + +open import Cubical.Core.Everything +open import Cubical.Data.Unit renaming (Unit to ⊤) +open import Cubical.Data.Empty +open import Cubical.Data.Nat hiding (isEven) + +isEven : ℕ → Type +isEven zero = ⊤ +isEven (suc zero) = ⊥ +isEven (suc (suc n)) = isEven n + + +existsEven : Σ ℕ isEven +existsEven = 4 , tt + +div2 : Σ ℕ isEven → ℕ +div2 (0 , tt) = 0 +div2 (suc (suc n) , hn) = suc (div2 (n , hn)) diff --git a/Trinitarianism/images/isEven.png b/Trinitarianism/images/isEven.png new file mode 100644 index 0000000..4e7153e Binary files /dev/null and b/Trinitarianism/images/isEven.png differ diff --git a/Trinitarianism/images/isEvenBundle.png b/Trinitarianism/images/isEvenBundle.png new file mode 100644 index 0000000..a2e8e02 Binary files /dev/null and b/Trinitarianism/images/isEvenBundle.png differ diff --git a/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai b/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai index 816ddff..10f54e5 100644 Binary files a/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai and b/_build/2.6.2/agda/Trinitarianism/Quest0Solutions.agdai differ diff --git a/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai b/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai new file mode 100644 index 0000000..fc48c05 Binary files /dev/null and b/_build/2.6.2/agda/Trinitarianism/Quest1Solutions.agdai differ