# Quest 3 - Pi Types

We will try to formulate and prove the statement

Problem statement

The sum of two even naturals is even.

## Part 0 - 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 `ℕ → ℕ → ℕ`

.

```
_+_ : ℕ → ℕ → ℕ
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`

.

## Part 1 - The Statement

Now we can make the statement that a sum of even naturals is even in `agda`

.
Make sure it is of the form

```
Name : Statement
Name = ?
```

The statement should be of the form `(x y : A) → B`

where `A`

represents the subset of even naturals
and `B`

expresses what it means for the “sum of `x`

and `y`

” to be even.

## Hint

Given `x y : Σ ℕ isEven`

we want to show that their sum
(really the sum of their fist components) is even,
so we should give `isEven (x .fst + y .fst)`

Tip

`x .fst`

is another notation for `fst x`

.
This works for all sigma types.

There are three ways to interpret this:

## Spoiler

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

.

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 interpretations :

it is the proposition “for all

`x : A`

, we have`B x`

”, and each term of the pi type 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!

## Part 2 - 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 each`+`

changed to`+'`

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

Important Question

But `_+_`

and `_+'_`

compute the same values.
Are `_+_`

and `_+'_`

“the same”? What is “the same”?