removed md files in trinitarianism
This commit is contained in:
Jlh18
parent
56834bcd40
commit
734b1a6a61
@ -1,229 +0,0 @@
|
||||
# Terms and Types
|
||||
|
||||
There are three ways of looking at `A : Type`.
|
||||
|
||||
- proof theoretically, '`A` is a proposition'
|
||||
- type theoretically, '`A` is a construction'
|
||||
- categorically, '`A` is an object in category `Type`'
|
||||
|
||||
A first example of a type construction is the function type.
|
||||
Given types `A : Type` and `B : Type`,
|
||||
we have another type `A → B : Type` which can be seen as
|
||||
|
||||
- the proposition '`A` implies `B`'
|
||||
- the construction 'ways to convert `A` recipes to `B` recipes'
|
||||
- internal hom of the category `Type`
|
||||
|
||||
To give examples of this, let's make some types first!
|
||||
|
||||
## True / Unit / Terminal object
|
||||
|
||||
```agda
|
||||
data ⊤ : Type where
|
||||
tt : ⊤
|
||||
```
|
||||
|
||||
It reads '`⊤` is an inductive type with a constructor `tt`',
|
||||
with three interpretations
|
||||
|
||||
- `⊤` 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,
|
||||
|
||||
- `a` is a proof of the proposition `A`
|
||||
- `a` is a recipe for the construction `A`
|
||||
- `a` is a generalised element of the object `A` in the category `Type`.
|
||||
|
||||
The above tells you how we _make_ a term of type `⊤`.
|
||||
Let's see an example of _using_ a term of type `⊤`:
|
||||
|
||||
```agda
|
||||
TrueToTrue : ⊤ → ⊤
|
||||
TrueToTrue = { }
|
||||
```
|
||||
|
||||
- enter `C-c C-l` (this means `Ctrl-c Ctrl-l`).
|
||||
Whenever you do this, Agda will check the document is written correctly.
|
||||
This will open the `*Agda Information*` window looking like
|
||||
|
||||
```
|
||||
?0 : ⊤ → ⊤
|
||||
?1 : ⊤
|
||||
?2 : ⊤
|
||||
```
|
||||
|
||||
This says you have three unfilled holes.
|
||||
- Now you can fill the hole `{ }0`.
|
||||
- navigate to the hole `{ }` using `C-c C-f` (forward) or `C-c C-b` (backward)
|
||||
- enter `C-c C-r`. The `r` stands for _refine_.
|
||||
Whenever you do this whilst having your cursor in a hole,
|
||||
Agda will try to help you.
|
||||
- you should see `λ x → { }`. This is agda's notation for `x ↦ { }`
|
||||
and is called `λ` abstraction, think `λ` for 'let'.
|
||||
- navigate to the new hole
|
||||
- enter `C-c C-,` (this means `Ctrl-c Ctrl-comma`).
|
||||
Whenever you make this command whilst having your cursor in a hole,
|
||||
Agda will check the _goal_.
|
||||
- the goal (`*Agda information*` window) should look like
|
||||
|
||||
```
|
||||
Goal: ⊤
|
||||
—————————————————————————
|
||||
x : ⊤
|
||||
```
|
||||
|
||||
you have a proof/recipe/generalized element `x : ⊤`
|
||||
and you need to give a proof/recipe/generalized element of `⊤`
|
||||
- write the proof/recipe/generalized element `x` of `⊤` in the hole
|
||||
- press `C-c C-SPC` to fill the hole with `x`.
|
||||
In general when you have some term (and your cursor) in a hole,
|
||||
doing `C-c C-SPC` will tell Agda to replace the hole with that term.
|
||||
Agda will give you an error if it can't make sense of your term.
|
||||
- the `*Agda Information*` window should now only have two unfilled holes left,
|
||||
this means Agda has accepted your proof.
|
||||
|
||||
```
|
||||
?1 : ⊤
|
||||
?2 : ⊤
|
||||
```
|
||||
|
||||
There is more than one proof (see `Quest0Solutions.agda`).
|
||||
Here is an important one:
|
||||
|
||||
```agda
|
||||
TrueToTrue' : ⊤ → ⊤
|
||||
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'.
|
||||
Doing `C-c C-c` with `x` in the hole
|
||||
tells agda to 'do cases on `x`'.
|
||||
The only case is `tt`.
|
||||
|
||||
One proof says for any term `x : ⊤` give `x` again.
|
||||
The other says it suffices to do the case of `tt`,
|
||||
for which we just give `tt`.
|
||||
|
||||
> Are these proofs 'the same'? What is 'the same'?
|
||||
|
||||
(This question is deep and should be unsettling.
|
||||
Sneak peek: they are _internally_ but
|
||||
not _externally_ 'the same'.)
|
||||
|
||||
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 `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.
|
||||
|
||||
## False / Empty / Initial object
|
||||
|
||||
```agda
|
||||
|
||||
data ⊥ : Type where
|
||||
|
||||
```
|
||||
|
||||
It reads '`⊥` is an inductive type with no constructors',
|
||||
with three interepretations
|
||||
|
||||
- `⊥` is a proposition with no proofs
|
||||
- `⊥` is a construction with no recipes
|
||||
- There are no generalized elements of `⊥` (it is a strict initial object)
|
||||
|
||||
Let's try mapping out of `⊥`.
|
||||
|
||||
```agda
|
||||
explosion : ⊥ → ⊤
|
||||
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 `Quest0Solutions.agda`)
|
||||
This has three interpretations:
|
||||
|
||||
- false implies anything (principle of explosion)
|
||||
- One can convert recipes of `⊥` to recipes of
|
||||
any other construction since
|
||||
there are no recipes of `⊥`.
|
||||
- `⊥` is initial in the category `Type`
|
||||
|
||||
## The natural numbers
|
||||
|
||||
We can also encode "natural numbers" as a type.
|
||||
|
||||
```agda
|
||||
data ℕ : Type where
|
||||
zero : ℕ
|
||||
suc : ℕ → ℕ
|
||||
```
|
||||
|
||||
As a construction, this reads :
|
||||
|
||||
- `ℕ` is a type of construction
|
||||
- `zero` is a recipe for `ℕ`
|
||||
- `suc` takes an existing recipe for `ℕ` and gives
|
||||
another recipe for `ℕ`.
|
||||
|
||||
We can also see `ℕ` categorically :
|
||||
ℕ is a natural numbers object in the category `Type`.
|
||||
This means it is equipped with morphisms `zero : ⊤ → ℕ`
|
||||
and `suc : ℕ → ℕ` such that
|
||||
given any `⊤ → A → A` there exist a unique morphism `ℕ → A`
|
||||
such that the diagram commutes:
|
||||
|
||||
<img src="images/nno.png"
|
||||
alt="nno"
|
||||
width="500"
|
||||
class="center"/>
|
||||
|
||||
`ℕ` 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'?
|
||||
|
||||
@ -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
|
||||
|
||||
<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.
|
||||
|
||||
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`.
|
||||
|
||||
<img src="images/generalBundle.png"
|
||||
alt="Bundle"
|
||||
width="500"/>
|
||||
|
||||
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.
|
||||
@ -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
|
||||
|
||||
<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'?
|
||||
|
||||
## 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.
|
||||
@ -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.
|
||||
<p>
|
||||
<details>
|
||||
<summary>Hint</summary>
|
||||
|
||||
`n + 0` should be `n` and `n + (m + 1)` should be `(n + m) + 1`
|
||||
</details>
|
||||
</p>
|
||||
|
||||
## The Statement
|
||||
|
||||
Now we can make the statement:
|
||||
```agda
|
||||
SumOfEven : (x : Σ ℕ isEven) → (y : Σ ℕ isEven) → isEven (x .fst + y .fst)
|
||||
SumOfEven x y = ?
|
||||
```
|
||||
> 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.
|
||||
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`),
|
||||
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!
|
||||
|
||||
## Remarks
|
||||
|
||||
_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?
|
||||
|
||||
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'?
|
||||
|
||||
## Another Task : Decidability of `isEven`
|
||||
|
||||
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`
|
||||
```agda
|
||||
data _⊕_ (A : Type) (B : Type) : Type where
|
||||
???
|
||||
```
|
||||
- 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
|
||||
|
||||
@ -1,49 +0,0 @@
|
||||
|
||||
Trinitarianism
|
||||
==============
|
||||
By the end of this arc we will (almost) have 'a place to do maths'.
|
||||
The 'types' that will populated this 'place'
|
||||
will have three interpretations:
|
||||
- Proof theoretically, with types as propositions
|
||||
- Type theoretically, with types as programs
|
||||
- Category theoretically, with types as objects in a category
|
||||
|
||||
<img src="images/trinitarianism.png"
|
||||
alt="the holy trinity"
|
||||
width="500"
|
||||
class="center"/>
|
||||
|
||||
## 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.
|
||||
Loading…
Reference in New Issue
Block a user