module hwk1 where

open import Data.Nat
open import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning

natrec : {C : Set} → (a : ℕ) → (d : C) → (e : ℕ → C → C) → C
natrec zero d e = d
natrec (suc b) d e = e b (natrec b d e)

⊕ : ℕ → ℕ → ℕ
⊕ x y = natrec x y (λ u v → suc v)

problem2-lemma : (x : ℕ) → natrec x 0 (λ u v → suc v) ≡ x
problem2-lemma zero = refl
problem2-lemma (suc x) = cong suc (problem2-lemma x)

-- (λ u v → suc v) x (natrec x 0 (λ u v → suc v))
-- suc (natrec x 0 (λ u v → suc v))
 
problem2 : (x : ℕ) → ⊕ x 0 ≡ x
problem2 x = problem2-lemma x
--   begin
--     ⊕ x 0
--   ≡⟨⟩
--     natrec x 0 (λ u v → suc v)
--   ≡⟨ {!   !} ⟩
--     x
--   ∎