# Quest 3 - Side Quests

## Decidability of `isEven`

Try to express and prove in `agda`

the statement

Problem statement

Every natural number is even or not even.

We make a summary of what is needed:

a definition of the type

`A ⊕ B`

(input`\oplus`

), which has interpretationsthe proposition “

`A`

or`B`

”the construction with two ways of making recipes

`left : A → A ⊕ B`

and`right : B → A ⊕ B`

.the disjoint sum of two spaces

the coproduct of two objects

`A`

and`B`

. The type needs to take in parameters`A : Type`

and`B : Type`

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