module nat where
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

indℕ : ∀ {ℓ} → (C : ℕ → Set ℓ) → C 0 → ((n : ℕ) → C n → C (suc n)) → (n : ℕ) → C n
indℕ C z f 0 = z
indℕ C z f (suc n) = f n (indℕ C z f n)

iter : ∀ {ℓ} (C : Set ℓ) → C → (C → C) → ℕ → C
iter C c₀ cs zero = c₀
iter C c₀ cs (suc n) = cs (iter C c₀ cs n)

recℕ₁ : ∀ {ℓ} (C : Set ℓ) → C → (ℕ → C → C) → ℕ → C
recℕ₁ C c₀ cs zero = c₀
recℕ₁ C c₀ cs (suc n) = cs n (recℕ₁ C c₀ cs n)

recℕ₂ : ∀ {ℓ} (C : Set ℓ) → C → (ℕ → C → C) → ℕ → C
recℕ₂ C c₀ cs n = proj₁ (iter (C × ℕ) (c₀ , 0) (λ p → cs (proj₂ p) (proj₁ p) , suc (proj₂ p)) n)

recℕ₁≡recℕ₂ : ∀ {ℓ} (C : Set ℓ) → (c : C) → (cs : (ℕ → C → C)) → (n : ℕ) → recℕ₁ C c cs n ≡ recℕ₂ C c cs n
recℕ₁≡recℕ₂ C c cs = indℕ (λ n → recℕ₁ C c cs n ≡ recℕ₂ C c cs n) refl (λ n → {!!})