-
-`ℕ` has no interpretation as a proposition since
-there are 'too many proofs' -
-mathematicians classically don't distinguish
-between proofs of a single proposition.
-(ZFC doesn't even mention logic internally,
-unlike Type Theory!)
-
-To see how to use terms of type `ℕ`, i.e. induction on `ℕ`,
-go to Quest1!
-
-## Universes
-
-You may have noticed the notational similarities between
-`zero : ℕ` and `ℕ : Type`.
-This may have lead you to the question, `Type : ?`.
-In type theory, we simply assert `Type : Type₁`.
-But then we are chasing our tail, asking `Type₁ : Type₂`.
-Type theorists make sure that every type
-(i.e. anything the right side of `:`)
-itself is a term (i.e. anything on the left of `:`),
-and every term has a type.
-So what we really need is
-```
-Type : Type₁, Type₁ : Type₂, Type₂ : Type₃, ⋯
-```
-These are called _universes_.
-The numberings of universes are called _levels_.
-It will be crucial that types can be treated as terms.
-This will allows us to
-
- - reason about '_structures_' such as 'the structure of a group',
- think 'for all groups'
- - do category theory without stepping out of the theory
- (no need for classes etc. For experts, we have Grothendieck universes.)
- - reason about when two types are 'the same',
- for example when are two definitions of
- the natural numbers 'the same'? What is 'the same'?
-
diff --git a/0Trinitarianism/Quest1.md b/0Trinitarianism/Quest1.md
deleted file mode 100644
index e533926..0000000
--- a/0Trinitarianism/Quest1.md
+++ /dev/null
@@ -1,135 +0,0 @@
-# Dependent Types
-
-In a 'place to do maths'
-we would like to be able to express and 'prove'
-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_.
-In general a predicate on a type `A : Type` is
-a term of type `A → Type`.
-For example,
-
-```agda
-isEven : ℕ → Type
-isEven n = ?
-```
-
-- Do `C-c C-l` to load the file.
-- Navigate to the hole.
-- Input `n` in the hole and do `C-c C-c`.
- You should now see
-
- ```agda
-
- isEven : ℕ → Type
- isEven zero = {!!}
- isEven (suc n) = {!!}
-
- ```
- 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 `ℕ`."
- This has the following interpretations :
-
- - propositionally, this is the _principle of mathematical induction_.
- - categorically, this is the universal property of a
- natural numbers object.
-
-- Navigate to the first hole and check the goal.
- You should see
- ```
- Goal: Type
- ———————————
- ```
- Fill the hole with `⊤`, since we want `zero` to be even.
-- Navigate to the second hole.
-- Input `n` and do `C-c C-c` again.
- You should now see
- ```agda
- isEven : ℕ → Type
- isEven zero = ⊤
- isEven (suc zero) = {!!}
- isEven (suc (suc n)) = {!!}
- ```
- 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 `⊥`,
- since we don't want `suc zero` to be even.
-- Navigate to the next hole and check the goal.
- You should see in the 'agda information' window,
- ```
- Goal: Type
- ——————————————
- n : ℕ
- ```
- We are in the 'inductive step',
- so we have access to the previous natural number.
-- Fill the hole with `isEven n`,
- since we want `suc (suc n)` to be even _precisely when_
- `n` is even.
-
- The reason we have access to the term `isEven n` is again
- 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 in `Quest2Solutions.agda`.)
-
-There are three interpretations of `isEven : ℕ → Type`.
-- Already mentioned, `isEven` is a predicate on `ℕ`.
-- `isEven` is a _dependent construction_.
- Specifically, `isEven n` is either `⊤` or `⊥` depending on `n : ℕ`.
-- `isEven` is a _bundle over `ℕ`_,
- i.e. an object in the over-category `Type↓ℕ`.
- Pictorially, it looks like
-
- 
-
- 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.
-
-In general given a type `A : Type`,
-a _dependent type `F` over `A`_ is a term `F : A → Type`.
-This should be drawn as a collection of space parameterised
-by the space `A`.
-
- 
-
-You can check if `2` is even by asking agda to 'reduce' the term `isEven 2`:
-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.)
-
-## Using the Trinitarianism
-
-We introduced new ideas through all three perspectives,
-as each has their own advantage
-
-- Types as propositions is often the most familiar perspective,
- and hence can offer guidance for the other two perspectives.
- However the current mathematical paradigm uses proof irrelevance
- (two proofs of the same proposition are always 'the same'),
- which is _not_ compatible with HoTT.
-- Types as constructions conveys the way in which 'data' is important,
- and should be preserved.
-- Types as objects allows us to draw pictures,
- thus guiding us through the syntax with geometric intuition.
-
-For each new idea introduced,
-make sure to justify it proof theoretically, type theoretically and
-categorically.
diff --git a/0Trinitarianism/Quest2.md b/0Trinitarianism/Quest2.md
deleted file mode 100644
index 8698dc1..0000000
--- a/0Trinitarianism/Quest2.md
+++ /dev/null
@@ -1,181 +0,0 @@
-# Sigma Types
-
-We are still trying to express and 'prove' the statement
-
-> There exists a natural that is even.
-
-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
-```
-∃ 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
-
- 
-
- 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'?
-
-## 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/Quest3.md b/0Trinitarianism/Quest3.md
deleted file mode 100644
index 6c12117..0000000
--- a/0Trinitarianism/Quest3.md
+++ /dev/null
@@ -1,120 +0,0 @@
-# Pi Types
-
-We will try to formulate and prove the statement
-
-> The sum of two even naturals is even.
-
-## Defining Addition
-
-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 = ?
-```
-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`
-
-
-## Terms and Types
-
-Here are some things that we could like to have in a 'place to do maths'
- - objects to reason about (E.g. `ℕ`)
- - recipes for making things inside objects
- (E.g. `n + m` for `n` and `m` in naturals.)
- - propositions to reason with (E.g. `n = 0` for `n` in naturals.)
-
-In proof theory, types are propositions and terms of a type are their proofs.
-In type theory, types are programs / constructions and
-terms are algorithms / recipes.
-In category theory, types are objects and terms are generalised elements.
-
-## Non-dependent Types
-
-- false / empty / initial object
-- true / unit / terminal object
-- or / sum / coproduct
-- and / pairs / product
-- implication / functions / internal hom
-
-## Dependent Types
-
-- predicate / type family / bundle
-- substitution / substitution / pullback (of bundles)
-- existence / Σ type / total space of bundles
-- for all / Π type / space of sections of bundles
-
-## What is 'the Same'?
-
-There will be one thing missing from this 'place to do maths'
-and that is a notion of _equality_.
-How HoTT treats equality is where it deviates from its predecessors.
-This is the theme of the next arc.