Quest 3 - Pi Types
We will try to formulate and prove the 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.
n + 0 should be
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
Make sure it is of the form
Name : Statement Name = ?
The statement should be of the form
(x y : A) → B where
represents the subset of even naturals
B expresses what it means for the “sum of
y” to be even.
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)
x .fst is another notation for
This works for all sigma types.
There are three ways to interpret this:
For all even naturals
their sum is even.
isEven (x .fst + y .fst) is a construction depending on two recipes
Given two recipes
Σ ℕ 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).
For all even naturals
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.
(x : A) → B xare made by converting each
x : Ato some recipe of
B x. Indeed the function type
A → Bis the special case where the type
B xis 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 Bwhich is equipped with a projection
fst : Σ A B → A. A term of
(x : A) → B xis a section of this projection.
We are now in a position to prove the statement. Have fun!
Part 2 - Remarks
Once you have proven the statement,
check out our two ways of defining addition
(in the solutions).
C-c C-nto check that they compute the same values on different examples.
Uncomment the code for
Sum'OfEvenin the solutions. It is just
SumOfEvenbut with each
Load the file. Does the proof still work?
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.
_+'_ compute the same values.
_+'_ “the same”? What is “the same”?