# 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”?