-
- 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,
diff --git a/0Trinitarianism/Quest2.agda b/0Trinitarianism/Quest2.agda
index 8134556..42474dd 100644
--- a/0Trinitarianism/Quest2.agda
+++ b/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 = {!!}
diff --git a/0Trinitarianism/Quest2.md b/0Trinitarianism/Quest2.md
index 08630c5..8698dc1 100644
--- a/0Trinitarianism/Quest2.md
+++ 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.
-
-Hint
-
-`n + 0` should be `n` and `n + (m + 1)` should be `(n + m) + 1`
-
+
+ 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.
diff --git a/0Trinitarianism/Quest2Solutions.agda b/0Trinitarianism/Quest2Solutions.agda
index 2d9f39b..a16b238 100644
--- a/0Trinitarianism/Quest2Solutions.agda
+++ b/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)
diff --git a/0Trinitarianism/Quest3.md b/0Trinitarianism/Quest3.md
index 9a6a312..6c12117 100644
--- a/0Trinitarianism/Quest3.md
+++ 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!
diff --git a/Plan.org b/Plan.org
index 53360dc..c819cdf 100644
--- a/Plan.org
+++ b/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
diff --git a/_build/2.6.3/agda/0Trinitarianism/Preambles/P2.agdai b/_build/2.6.3/agda/0Trinitarianism/Preambles/P2.agdai
new file mode 100644
index 0000000..d22d6a5
Binary files /dev/null and b/_build/2.6.3/agda/0Trinitarianism/Preambles/P2.agdai differ
diff --git a/_build/2.6.3/agda/0Trinitarianism/Quest2Solutions.agdai b/_build/2.6.3/agda/0Trinitarianism/Quest2Solutions.agdai
new file mode 100644
index 0000000..c0efbe6
Binary files /dev/null and b/_build/2.6.3/agda/0Trinitarianism/Quest2Solutions.agdai differ