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

• the 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