# Exercises in Type Theory

These exercises should help you get familiar with type theory as a language for
writing down mathematical structures, constructions, statements, and proofs. If
you are only beginning to use type theory, you will likely have many questions,
as even simple notational conventions and basics will be new to you. We
encourage you to work together with others, and to ask lots of questions!

You should try to solve the exercises on paper as well as with Coq (see
the accompanying file Spartan_exercises.v). The paper
is good for understanding and Coq is good for precision.

### Exercise 1

For each of the following types, write down an element of that type, if it has
one. If it does not have any elements, you should establish that this is the
case. Recall the lecture: to show that A has no elements, we construct an
element of `A → empty`

.

`A × (B + C) → A × B + A × C`

, given types `A`

, `B`

, and `C`

`(A → A) → (A → A)`

, given type `A`

(for extra credit, write down *five* elements of this type)
`Id_nat (0, succ 0)`

`∑ (A : Universe) (A → empty) → empty`

`∏ (n : nat), ∑ (m : nat), Id_nat n (2 · m) + Id_nat n (2 · m + 1)`

, assuming you have got arithmetic.
`(∑ (x : A) B × P x) → B × ∑ (x : A) P x`

, given types `A`

, `B`

, and `P : A → Universe`

`B → (B → A) → A`

, given types `A`

and `B`

`B → ∏ (A : Universe) (B → A) → A`

, given type `B`

`(∏ (A : Universe) (B → A) → A) → B`

, given type `B`

### Exercise 2

- Using the basic rules for natural numbers, construct addition on natural numbers.
- State associativity and commutativity of addition in a type-theoretic way.

### Exercise 3

Write down the following types and elements:

- even natural numbers, and
`4`

as an element of this type
- prime numbers, and
`7`

as an element of this type
- functions
`A → nat`

with a given argument at which they are zero
(set-theoretically this would be `{ (x, f) ∈ A × (A → nat) | f x = 0 }`

).
- pairs
`(m, n)`

of natural numbers such that `m ≤ n`

, and `(2, 4)`

as an element of
this type.

### Exercise 4

We say that a dependent type `P : A → Universe`

is decidable if there is an element of
`∏ (x:A), P x + (P x → Empty)`

. Which of the following are decidable?

`P : bool → Universe`

, defined by `P true ≡ unit`

and `P false ≡ empty`

.
`P : nat → Universe`

, defined by `P n ≡ Id_nat (n, 42)`

.