Updated many things.

0Trinitarianism/Preambles/P2.agda

@@ -1,6 +1,6 @@
 module 0Trinitarianism.Preambles.P2 where
 
 open import Cubical.Core.Everything public
-open import Cubical.Data.Nat public hiding (_+_ ; isEven)
-open import 0Trinitarianism.Quest1Solutions public
+open import Cubical.Data.Unit public renaming (Unit to ⊤)
 open import Cubical.Data.Empty public using (⊥)
+open import Cubical.Data.Nat public hiding (isEven)

0Trinitarianism/Quest0.md

@@ -90,7 +90,7 @@ TrueToTrue = { }
   ?2 : ⊤
   ```
 
-There is more than one proof (see solutions).
+There is more than one proof (see `Quest0Solutions.agda`).
 Here is an important one:
 
 ```agda
@@ -150,7 +150,8 @@ explosion x = { }
 
   - Navigate to the hole and do cases on `x`.
 
-Agda knows that there are no cases so there is nothing to do (see solutions)!
+Agda knows that there are no cases so there is nothing to do!
+(See `Quest0Solutions.agda`)
 This has three interpretations:
 
   - false implies anything (principle of explosion)

0Trinitarianism/Quest1.md

@@ -1,4 +1,4 @@
-# Dependent Types and Sigma Types
+# Dependent Types
 
 In a 'place to do maths'
 we would like to be able to express and 'prove'
@@ -6,6 +6,9 @@ the statement
 
 > There exists a natural that is even.
 
+The goal of this quest is to define
+"what it means for a natural to be even".
+
 ## Predicates / Dependent Constructions / Bundles
 
 This requires the notion of a _predicate_.
@@ -79,7 +82,7 @@ isEven n = ?
   because we are in the 'inductive step'.
 - There should now be nothing in the 'agda info' window.
   This means everything is working. 
-  (Compare your `isEven` with our [solutions]().)
+  (Compare your `isEven` with our solutions in `Quest2Solutions.agda`.)
 
 There are three interpretations of `isEven : ℕ → Type`.
 - Already mentioned, `isEven` is a predicate on `ℕ`.
@@ -112,136 +115,6 @@ 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.)
 
-## Sigma Types
-
-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 construction 
-  'keep a recipe `n` of naturals together with a recipe of `isEven n`'
-- the total space of the bundle `isEven` over `ℕ`,
-  which is the space obtained by putting together 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 terms in Sigma Types
-Making a term of this type has three interpretations:
-
-- a natural `n : ℕ` together with a proof `hn : isEven n` that `n` is even.
-- a recipe `n : ℕ` together with 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 the sigma type `Σ A B` whose terms are pairs `a , b` 
-where `a : A` and `b : B a`. 
-In the special case when `B` is not dependent on `a : A`,
-i.e. it looks like `λ a → C` for some `C : Type` then 
-`Σ A B` is just 
-- the proposition '`A` and `C`' 
-  since giving a proof of this is the same as giving a proof 
-  of `A` and a proof of `C`
-- a recipe `a : A` together with a recipe `c : C`
-- `B` is now a _trivial bundle_ since the fibers `B a` are 
-  constant with respect to `a : A`.
-  In other words it is just a _product_ `Σ A B ≅ A × C`.
-  For this reason, 
-  some refer to the sigma type as the _dependent product_,
-  but we will avoid this terminology.
-```agda
-_×_ : Type → Type → Type
-A × C = Σ A (λ a → C)
-```
-Agda supports the notation `_×_` (without spaces)
-which means from now on you can write `A × C` (with spaces).
-
-### Using Terms in Sigma Types
-
-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`.
-Given `x : Σ A B` there are three interpretations of `fst` and `snd`:
-- Viewing `x` as a proof of existence
-  `fst x` provides the witness of existence and `snd` provides the proof 
-  that the witness `fst x` has the desired property
-- Viewing `x` as a recipe `fst` extracts the first component and 
-  `snd` extracts the second component 
-- Viewing `x` as a point in the total space of a bundle 
-  `fst x` is the point that `x` is over in the base space and `snd x`
-  is the point in the fiber that `x` represents.
-  In particular you can interpret `fst` as projection from the total space
-  to the base space, collapsing fibers.
-For example to define a map that takes an even natural and divides it by two 
-we can do 
-```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 agda what to give for `0 , _`,
-  i.e. what 'zero divided by two' ought to be.
-  ```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.
-  ```agda
-  div2 : Σ ℕ isEven → ℕ
-  div2 (zero , snd₁) = 0
-  div2 (suc (suc fst₁) , snd₁) = {!!}
-  ```
-- `(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)`,
-and hence `1` would be 'the same' as `18`. 
-
-> Are they 'the same'? What is 'the same'? 
-
 ## Using the Trinitarianism
 
 We introduced new ideas through all three perspectives,

0Trinitarianism/Quest2.agda

@@ -2,8 +2,27 @@ module 0Trinitarianism.Quest2 where
 
 open import 0Trinitarianism.Preambles.P2
 
-_+_ : ℕ → ℕ → ℕ
-n + m = {!!}
+isEven : ℕ → Type
+isEven n = {!!}
 
-SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst)
-SumOfEven x y = {!!}
+{-
+This is a comment block.
+Remove this comment block and formulate
+'there exists an even natural' here.
+-}
+
+_×_ : Type → Type → Type
+A × C = Σ A (λ a → C)
+
+div2 : Σ ℕ isEven → ℕ
+div2 x = {!!}
+
+private
+  postulate
+    A B C : Type
+
+uncurry : (A → B → C) → (A × B → C)
+uncurry f x = {!!}
+
+curry : (A × B → C) → (A → B → C)
+curry f a b = {!!}

0Trinitarianism/Quest2.md

@@ -1,92 +1,181 @@
-# Pi Types
+# Sigma Types
 
-We will try to formulate and prove the statement 
+We are still trying to express and 'prove' the statement
 
-> The sum of two even naturals is even.
+> There exists a natural that is even.
 
-To do so we must define `+` on the naturals.
-Addition takes in two naturals and spits out a natural, 
-so it should have type `ℕ → ℕ → ℕ`.
-```agda
-_+_ : ℕ → ℕ → ℕ
-n + m = ?
+We will achieve this by the end of this quest.
+
+## Existence / Dependent Pair / Total Space of Bundles
+
+Recall from [Quest 1](
+https://github.com/thehottgame/TheHoTTGame/blob/main/0Trinitarianism/Quest1.md
+)
+that we defined `isEven`.
+What's left is to be able write down "existence".
+In maths we might write 
 ```
-Try coming up with a sensible definition.
-It may not look 'the same' as ours.
-<p>
-<details>
-<summary>Hint</summary>
-
-`n + 0` should be `n` and `n + (m + 1)` should be `(n + m) + 1`
-</details>
-</p>
-
-Now we can make the statement:
-```agda
-SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst)
-SumOfEven x y = ?
+∃ x ∈ ℕ, isEven x
 ```
-> Tip: `x .fst` is another notation for `fst x`.
-> This works for all sigma types.
-There are three ways to interpret this:
-- For all even naturals `x` and `y`, 
-  their sum is even.
-- `isEven (x .fst + y .fst)` is a construction depending on two recipes
-  `x` and `y`.
-  Given two recipes `x` and `y` of `Σ ℕ isEven`, 
-  we break them down into their first components,
-  apply the conversion `_+_`,
-  and form a recipe for `isEven` of the result.
-- `isEven (_ .fst + _ .fst)` is a bundle over the categorical product
-  `Σ ℕ isEven × Σ ℕ isEven` and `SumOfEven` is a _section_ of the bundle.
+which in agda notation is 
+```
+Σ ℕ isEven
+```
+This is called a _sigma type_, which has three interpretations:
+
+- the proposition 'there exists an even natural'
+- the construction 
+  'keep a recipe `n` of naturals together with a recipe of `isEven n`'
+- the total space of the bundle `isEven` over `ℕ`,
+  which is the space obtained by putting together all the fibers.
+  Pictorially, it looks like
   
-More generally given `A : Type` and `B : A → Type`
-we can form the _pi type_ `(x : A) → B x : Type` 
-(in other languages `Π (x : ℕ), isEven n`). 
-The notation suggests that these behave like functions,
-and indeed in the special case where the fiber is constant 
-with respect to the base space 
-a section is just a term of type `A → B`, i.e. a function. 
-Hence pi types are also known as _dependent function types_.
+  <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_).
 
-We are now in a position to prove the statement. Have fun!
+## Making terms in Sigma Types
+Making a term of this type has three interpretations:
 
-_Important_: Once you have proven the statement, 
-check out our two ways of defining addition `_+_` and `_+'_`
-(in the solutions).
-- Use `C-c C-n` to check that they compute the same values
-  on different examples.
-- Uncomment the code for `Sum'OfEven` in the solutions.
-  It is just `SumOfEven` but with `+`s changed for `+'`s.
-- Load the file. Does the proof still work?
+- a natural `n : ℕ` together with a proof `hn : isEven n` that `n` is even.
+- a recipe `n : ℕ` together with 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.
 
-Our proof `SumOfEven` relied on 
-the explicit definition of `_+_`,
-which means if we wanted to use our proof on 
-someone else's definition of addition, 
-it might not work anymore.
-> But `_+_` and `_+'_` compute the same values. 
-> Are `_+_` and `_+'_` 'the same'? What is 'the same'?
+Now you can prove that there exists an even natural:
 
-As the final task of the Quest,
-try to express and prove in agda the statement
-> For any natural number it is even or is is not even.
-We will make a summary of what is needed:
-- a definition of the type `A ⊕ B` (input `\oplus`),
-  which has three interpretations
-  - the proposition '`A` or `B`'
-  - the construction with two ways of making recipes 
-    `left : A → A ⊕ B`
-    and `right : B → A ⊕ B`.
-  - the coproduct of two objects `A` and `B`.
-  The type needs to take in parameters `A : Type` and `B : Type`
+- Formulate the statement you need. Make sure you have it of the form 
   ```agda
-  data _⊕_ (A : Type) (B : Type) : Type where
-    ???
+  Name : Statement
+  Name = ?
   ```
-- a definition of negation. One can motivate it by the following
-  - Define `A ↔ B : Type` for two types `A : Type` and `B : Type`.
-  - Show that for any `A : Type` we have `(A ↔ ⊥) ↔ (A → ⊥)`
-  - Define `¬ : Type → Type` to be `λ A → (A → ⊥)`.
-- a formulation and proof of the statement above
+- 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 the sigma type `Σ A B` whose terms are pairs `a , b` 
+where `a : A` and `b : B a`. 
+In the special case when `B` is not dependent on `a : A`,
+i.e. it looks like `λ a → C` for some `C : Type` then 
+`Σ A B` is just 
+- the proposition '`A` and `C`' 
+  since giving a proof of this is the same as giving a proof 
+  of `A` and a proof of `C`
+- a recipe `a : A` together with a recipe `c : C`
+- `B` is now a _trivial bundle_ since the fibers `B a` are 
+  constant with respect to `a : A`.
+  In other words it is just a _product_ `Σ A B ≅ A × C`.
+  For this reason, 
+  some refer to the sigma type as the _dependent product_,
+  but we will avoid this terminology.
+```agda
+_×_ : Type → Type → Type
+A × C = Σ A (λ a → C)
+```
+Agda supports the notation `_×_` (without spaces)
+which means from now on you can write `A × C` (with spaces).
+
+## Using Terms in Sigma Types
+
+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`.
+Given `x : Σ A B` there are three interpretations of `fst` and `snd`:
+- Viewing `x` as a proof of existence
+  `fst x` provides the witness of existence and `snd` provides the proof 
+  that the witness `fst x` has the desired property
+- Viewing `x` as a recipe `fst` extracts the first component and 
+  `snd` extracts the second component 
+- Viewing `x` as a point in the total space of a bundle 
+  `fst x` is the point that `x` is over in the base space and `snd x`
+  is the point in the fiber that `x` represents.
+  In particular you can interpret `fst` as projection from the total space
+  to the base space, collapsing fibers.
+For example to define a map that takes an even natural and divides it by two 
+we can do 
+```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 agda what to give for `0 , _`,
+  i.e. what 'zero divided by two' ought to be.
+  ```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.
+  ```agda
+  div2 : Σ ℕ isEven → ℕ
+  div2 (zero , snd₁) = 0
+  div2 (suc (suc fst₁) , snd₁) = {!!}
+  ```
+- `(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)`,
+and hence `1` would be 'the same' as `18`. 
+
+> Are they 'the same'? What is 'the same'? 
+
+## Side Quest : a Tautology / Currying / Cartesian Closed
+
+In this side quest, 
+you will construct the following functions.
+
+```agda
+uncurry : (A → B → C) → (A × B → C)
+uncurry f x = ?
+
+curry : (A × B → C) → (A → B → C)
+curry f a b = ?
+```
+These have three interpretations : 
+
+- `uncurry` is a proof that
+  "if `A` implies '`B` implies `C`',
+  then '`A` and `B`' implies `C`".
+  A proof of the converse is `curry`.
+- [currying](
+https://en.wikipedia.org/wiki/Currying#:~:text=In%20mathematics%20and%20computer%20science,each%20takes%20a%20single%20argument.)
+- this is a commonly occuring example of an _adjunction_.
+  See
+  [here](https://kl-i.github.io/posts/2021-07-12/#product-and-maps)
+  for a more detailed explanation.
+
+Note that we have _postulated_ the types `A, B, C` for you.
+```agda
+private
+  postulate
+    A B C : Type
+```
+In general, you can use this to
+introduce new constants to your agda file.
+The `private` ensures `A, B, C` can only be used
+within this agda file.
+
+> Tip : Agda is space-and-indentation sensitive,
+> i.e. the `private` applies to anything beneath it
+> that is indented two spaces.

0Trinitarianism/Quest2Solutions.agda

@@ -2,57 +2,27 @@ module 0Trinitarianism.Quest2Solutions where
 
 open import 0Trinitarianism.Preambles.P2
 
-_+_ : ℕ → ℕ → ℕ
-n + zero = n
-n + suc m = suc (n + m)
+isEven : ℕ → Type
+isEven zero = ⊤
+isEven (suc zero) = ⊥
+isEven (suc (suc n)) = isEven n
 
-_+'_ : ℕ → ℕ → ℕ
-zero +' n = n
-suc m +' n = suc (m +' n)
+existsEven : Σ ℕ isEven
+existsEven = 4 , tt
 
-SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst)
-SumOfEven x (zero , hy) = x .snd
-SumOfEven x (suc (suc y) , hy) = SumOfEven x (y , hy)
+_×_ : Type → Type → Type
+A × C = Σ A (λ a → C)
 
-{-
+div2 : Σ ℕ isEven → ℕ
+div2 (0 , tt) = 0
+div2 (suc (suc n) , hn) = suc (div2 (n , hn))
 
-Sum'OfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst +' y .fst)
-Sum'OfEven x (zero , hy) = x .snd
-Sum'OfEven x (suc (suc y) , hy) = Sum'OfEven x (y , hy)
+private
+  postulate
+    A B C : Type
 
--}
+uncurry : (A → B → C) → (A × B → C)
+uncurry f (fst₁ , snd₁) = f fst₁ snd₁
 
-data _⊕_ (A : Type) (B : Type) : Type where
-  left : A → A ⊕ B
-  right : B → A ⊕ B
-
-_↔_ : Type → Type → Type
-_↔_ A B = (A → B) × (B → A)
-
-¬Motivation : (A : Type) → ((A ↔ ⊥) ↔ (A → ⊥))
-¬Motivation A =
-  -- forward direction
-  (
-    -- suppose we have a proof `hiff : A ↔ ⊥`
-    λ hiff →
-    -- give the forward map only
-    fst hiff
-  ) ,
-  -- backward direction; assume a proof hto : A → ⊥
-  λ hto →
-    -- we need to show A → ⊥ which we have already
-    hto
-    ,
-    -- we need to show ⊥ → A, which is the principle of explosion
-    λ ()
-
-¬ : Type → Type
-¬ A = A → ⊥
-
-isEvenDecidable : (n : ℕ) → isEven n ⊕ ¬ (isEven n)
--- zero is even; go left
-isEvenDecidable zero = left tt
--- one is not even; go right
-isEvenDecidable (suc zero) = right (λ ())
--- inductive step
-isEvenDecidable (suc (suc n)) = isEvenDecidable n
+curry : (A × B → C) → (A → B → C)
+curry f a b = f (a , b)

0Trinitarianism/Quest3.md

@@ -44,15 +44,32 @@ There are three ways to interpret this:
   and form a recipe for `isEven` of the result.
 - `isEven (_ .fst + _ .fst)` is a bundle over the categorical product
   `Σ ℕ isEven × Σ ℕ isEven` and `SumOfEven` is a _section_ of the bundle.
+  This means for every point `(x , y)` in `Σ ℕ isEven × Σ ℕ isEven`,
+  it gives a point in the fiber `isEven (x .fst + y .fst)`.
+  
+  (picture)
   
 More generally given `A : Type` and `B : A → Type`
 we can form the _pi type_ `(x : A) → B x : Type` 
-(in other languages `Π (x : ℕ), isEven n`). 
-The notation suggests that these behave like functions,
-and indeed in the special case where the fiber is constant 
-with respect to the base space 
-a section is just a term of type `A → B`, i.e. a function. 
-Hence pi types are also known as _dependent function types_.
+(in other languages `Π (x : ℕ), isEven n`),
+with three interpretations : 
+
+- it is the proposition "for all `x : A`, we have `B x`",
+  and each term is a collection of proofs `bx : B x`,
+  one for each `x : A`.
+- recipes of `(x : A) → B x` are made by
+  converting each `x : A` to some recipe of `B x`.
+  Indeed the function type `A → B` is 
+  the special case where 
+  the type `B x` is not dependent on `x`. 
+  Hence pi types are also known as _dependent function types_.
+  Note that terms in the sigma type are pairs `(a , b)` 
+  whilst terms in the dependent function type are 
+  a collection of pairs `(a , b)` indexed by `a : A`
+- Given the bundle `B : A → Type`,
+  we have the total space `Σ A B` which is equipped with a projection
+  `fst : Σ A B → A`.
+  A term of `(x : A) → B x` is a section of this projection.
 
 We are now in a position to prove the statement. Have fun!
 

Plan.org

@@ -77,6 +77,9 @@
   + difficulty is that PathP not in one fiber, but PathOver is, AND PathOver <-> PathP NON-obvious
   + Easy to generalize situation to n-types being closed under Sigma (7.1.8 in HoTT book), we showed this assuming PathPIsoPath
 
+** Mixolydian Bosses
+
++ universe classifies bundles
 
 ** SuperUltraMegaHyperLydianBosses
 + natural number object unique and `_+_` unique on any nat num obj
@@ -90,7 +93,6 @@
     - propositions closed under sigma types
   + univalence
 
-
 ** Top 100 (set theoretic) misconceptions about type theory
 + Propositions
 + Proof relevance