How to prove that the defining equations of the recursor for N hold propositionally using the induction principle for N in Agda?

Question

This is an exercise from the Homotopy Type Theory book. Here's what I have:

data ℕ : Set where
    zero : ℕ
    succ : ℕ → ℕ

iter : {C : Set} → C → (C → C) → ℕ → C
iter z f  zero    = z
iter z f (succ n) = f (iter z f n)

succℕ : {C : Set} → (ℕ → C → C) → ℕ × C → ℕ × C
succℕ f (n , x) = (succ n , f n x)

iterℕ : {C : Set} → C → (ℕ → C → C) → ℕ → ℕ × C
iterℕ z f = iter (zero , z) (succℕ f)

recℕ : {C : Set} → C → (ℕ → C → C) → ℕ → C
recℕ z f = _×_.proj₂ ∘ iterℕ z f

indℕ : {C : ℕ → Set} → C zero → ((n : ℕ) → C n → C (succ n)) → (n : ℕ) → C n
indℕ z f  zero    = z
indℕ z f (succ n) = f n (indℕ z f n)

recℕzfzero≡z : {C : Set} {z : C} {f : ℕ → C → C} → recℕ z f zero ≡ z
recℕzfzero≡z = refl

recℕzfsuccn≡fnrecℕzfn : {C : Set} {z : C} {f : ℕ → C → C} (n : ℕ) →
                        recℕ z f (succ n) ≡ f n (recℕ z f n)
recℕzfsuccn≡fnrecℕzfn = indℕ refl ?

I don't know how to prove that recℕ z f (succ n) ≡ f n (recℕ z f n). I need to prove:

(n : ℕ) → recℕ z f (succ n) ≡ f n (recℕ z f n)
        → recℕ z f (succ (succ n)) ≡ f (succ n) (recℕ z f (succ n))

In English, given a natural number n and the induction hypothesis prove the consequent.

The infix operator _∘_ is normal function composition. The _≡_ and _×_ data types are defined as:

data _≡_ {A : Set} : A → A → Set where
    refl : {x : A} → x ≡ x

record _×_ (A B : Set) : Set where
    constructor _,_
    field
        _×_.proj₁ : A
        _×_.proj₂ : B

I've been thinking of a solution for quite a while but I can't figure out how to solve this problem.

Answer 1

Let's get some help from Agda-mode for emacs:

recℕzfsuccn≡fnrecℕzfn : {C : Set} {z : C} {f : ℕ → C → C} (n : ℕ) →
                        recℕ z f (succ n) ≡ f n (recℕ z f n)
recℕzfsuccn≡fnrecℕzfn {f = f} n = {!!}

If we normalize the context in the hole by typing C-u C-u C-c C-, (each time I feel like I'm trying to invoke fatality in Mortal Kombat), we'll see (I cleaned up your definitions a bit)

Goal: f
      (proj₁
       (iter (0 , .z) (λ nx → succ (proj₁ nx) , f (proj₁ nx) (proj₂ nx))
        n))
      (proj₂
       (iter (0 , .z) (λ nx → succ (proj₁ nx) , f (proj₁ nx) (proj₂ nx))
        n))
      ≡
      f n
      (proj₂
       (iter (0 , .z) (λ nx → succ (proj₁ nx) , f (proj₁ nx) (proj₂ nx))
        n))

The second arguments to f are equal at both sides, so we can write

recℕzfsuccn≡fnrecℕzfn {f = f} n = cong (λ m -> f m (recℕ _ f n)) {!!}

where

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

Now the goal is

Goal: proj₁ (iter (zero , .z) (succℕ f) n) ≡ n

which is a straightforward lemma

lem : {C : Set} {z : C} {f : ℕ → C → C} (n : ℕ)
    → proj₁ (iter (zero , z) (succℕ f) n) ≡ n
lem = indℕ refl (λ _ -> cong succ)

So

recℕzfsuccn≡fnrecℕzfn : {C : Set} {z : C} {f : ℕ → C → C} (n : ℕ) →
                        recℕ z f (succ n) ≡ f n (recℕ z f n)
recℕzfsuccn≡fnrecℕzfn {f = f} n = cong (λ m -> f m (recℕ _ f n)) (lem n)

The whole code.