module 0Trinitarianism.Quest3 where

open import 0Trinitarianism.Preambles.P3

_+_ : ℕ → ℕ → ℕ
n + zero = n
n + suc m = suc (n + m)

_+'_ : ℕ → ℕ → ℕ
zero +' m = m
suc n +' m = suc (n +' m)

{-
Write here your proof that the sum of
even naturals is even.
-}

SumOfEven : (x y : Σ ℕ isEven) → isEven (x .fst + y .fst)
SumOfEven x@(fst₁ , snd₁) (zero , snd₂) = snd₁
SumOfEven x@(fst₁ , snd₁) (suc (suc fst₂) , snd₂) = SumOfEven x ( fst₂ , snd₂)

data _⊕_ (A B : Type) : Type where
  inl : A → A ⊕ B
  inr : B → A ⊕ B

_⇔_ : Type → Type → Type
A ⇔ B = (A → B) × (B → A)

ex : {A : Type} → (A ⇔ ⊥) ⇔ (A → ⊥)
ex .fst = λ z → z .fst
ex .snd = λ x →  x , λ ()

¬ : Type → Type
¬ A = A → ⊥

proof : (x : ℕ) → (isEven x) ⊕ (¬ (isEven x))
proof zero = inl tt
proof (suc zero) = inr (λ ())
proof (suc (suc x)) = proof x