title: How to prove that the defining equations of the recursor for N hold propositionally using the induction principle for N in Agda?
body: <p>This is an exercise from the <a href="http://homotopytypetheory.org/" rel="nofollow">Homotopy Type Theory</a> book. Here's what I have:</p>
  
  <pre><code>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 ?
  </code></pre>
  
  <p>I don't know how to prove that <code>recℕ z f (succ n) ≡ f n (recℕ z f n)</code>. I need to prove:</p>
  
  <pre><code>(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))
  </code></pre>
  
  <p>In English, given a natural number <code>n</code> and the induction hypothesis prove the consequent.</p>
  
  <p>The infix operator <code>_∘_</code> is normal function composition. The <code>_≡_</code> and <code>_×_</code> data types are defined as:</p>
  
  <pre><code>data _≡_ {A : Set} : A → A → Set where
      refl : {x : A} → x ≡ x
  
  record _×_ (A B : Set) : Set where
      constructor _,_
      field
          _×_.proj₁ : A
          _×_.proj₂ : B
  </code></pre>
  
  <p>I've been thinking of a solution for quite a while but I can't figure out how to solve this problem.</p>