quest1 sigma types and div2

Trinitarianism/Quest0.agda

@@ -2,7 +2,7 @@ module Trinitarianism.Quest0 where
 open import Trinitarianism.Quest0Preamble
 
 data ⊤ : Type where
-  trivial : ⊤
+  tt : ⊤
 
 TrueToTrue : ⊤ → ⊤
 TrueToTrue = {!!}

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 proposition and there is a proof of it, called `tt`.
-  - `⊤` is a construction with a recipe called `trivial`
+  - `⊤` is a construction with a recipe called `tt`
-  - `⊤` is a terminal object: every object has a morphism into `⊤` given by `· ↦ trivial`
+  - `⊤` 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
+It says 'to map out of ⊤ it suffices to do the case when `x` is `tt`', or
-  - the only proof of `⊤` is `trivial`
+  - the only proof of `⊤` is `tt`
-  - the only recipe for `⊤` is `trivial`
+  - the only recipe for `⊤` is `tt`
-  - the only one generalized element `trivial` in `⊤`
+  - 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

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
 

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 = {!!}

Trinitarianism/Quest1.md

@@ -28,11 +28,11 @@ isEven n = ?
   isEven (suc n) = {!!}
 
   ```
-  Explanation : 'to define a function on `ℕ`,
+  It says "to define a function on `ℕ`,
-  it suffices to define the function on the __cases_, 
+  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
+
+  <img src="images/isEven.png" 
+     alt="isEven" 
+     width="500"/>
+     
+  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
+  <img src="images/isEvenBundle.png" 
+     alt="SigmaTypeOfIsEven" 
+     width="500"/>
+  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'? 
+<!-- see Arc/Quest smth? -->

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))