40 lines
912 B
Agda
40 lines
912 B
Agda
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
|