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