Defining the recursor for natural numbers using iterator (HoTT book exercise) This is exercise 1.4 from the Homotopy Type Theory book:

Assuming as given only the iterator for natural numbers: 
  $$ iter: \prod_{C:U} C\to (C \to C) \to \mathbb N \to C$$
  with defining equations:
  $$ iter(C,c_0,c_s,0):\equiv c_0 $$
  $$iter(C,c_0,c_s,succ(n)):\equiv c_s(iter(C,c_0,c_s,n)$$
  derive a function having the type of the recursor  $rec_{\mathbb N}$. Show that the defining equations of the recursor hold propositionally for this function, using the induction principle for $\mathbb N$.

To derive such a function, it seemed obvious that having a $c_s$ with only one input, our new $c_s ':\mathbb N \to C\to C$ will just ignore the first input, so it can be the same as the iterator's. This way however i have just renamed the iterator function that i had, even if the type now matches the recursor given in the book.
The second part of the exercise seems kind of weirdly stated. At first i assumed it meant that the new function must be propositionally equal to the recursor, but this i think cannot happen.
The recursor in the book is given as: $$ rec_{\mathbb N}: \prod_{C:U} C\to (\mathbb N \to C \to C) \to \mathbb N \to C$$
$$ rec_{\mathbb N}(C,c_0,c_s'',0):\equiv c_0 $$
$$rec_{\mathbb N}(C,c_0,c_s'',succ(n)):\equiv c_s ''(n,rec_{\mathbb N}(C,c_0,c_s'',n)$$
Let's say i define $$ rec_{\mathbb N}': \prod_{C:U} C\to (\mathbb N \to C \to C) \to \mathbb N \to C$$
$$ rec_{\mathbb N}'(C,c_0,c_s',0):\equiv c_0 \equiv iter(C,c_0,c_s,0)$$
$$rec_{\mathbb N}'(C,c_0,c_s',succ(n)):\equiv c_s'(n,rec_{\mathbb N}'(C,c_0,c_s',n):\equiv c_s(iter(C,c_0,c_s,n))$$
Does my definition make sense, in order for the second part of the exercise to work?
 A: You've misunderstood the exercise. I suspect you have a deeper confusion about the role of defining equations is generally, and what constitutes term of HoTT.
The $:\equiv$ notation is meta-notation. It is not part of the language of HoTT. Uses of $:\equiv$ notation are axiomatic assertions. A function in the language of HoTT would be some lambda term.
The exercise is saying: if we extend the language of HoTT with a new (undefined) term $iter$ such that everywhere you can replace $iter(C,c_0,c_s,0)$ with $c_0$ and vice versa and similarly for the other defining equation, can you produce a term, call it $rec_\mathbb{N}$, of the given type in this new extended language such that you can produce a value of type $rec_\mathbb{N}(C,c_0,c_s,0) = c_0$ and $rec_\mathbb{N}(C,c_0,c_s,succ(n)) = c_s(n,rec_\mathbb{N}(C,c_0,c_s,n))$ where I'm using $=$ for propositional equality? A solution to this will be a lambda term that you can substitute for $rec_\mathbb{N}$ (presumably with $iter$ as a subterm) for which you can prove those equalities (which, in HoTT, means produce a value of those propositional equality types).
As an example, deriving addition from $iter$ means producing a lambda term of type $\mathbb{N}\to\mathbb{N}\to\mathbb{N}$ that satisfies the laws of addition. In this case, $\lambda m:\mathbb{N}.\lambda n:\mathbb{N}.iter(\mathbb{N},m,succ,n)$ is such a lambda term, call it $add$. We can prove $add(x)(0)=_\mathbb{N}x$ immediately via reflexivity because $$\begin{align}
(\lambda m:\mathbb{N}.\lambda n:\mathbb{N}.iter(\mathbb{N},m,succ,n))(x)(0) 
& \equiv (\lambda n:\mathbb{N}.iter(\mathbb{N},x,succ,n))(0) \\
& \equiv iter(\mathbb{N},x,succ,0) \\
& \equiv x
\end{align}$$
where the first two definitional equalities are beta-reduction, and the last is the first defining equality of $iter$. However, proving $add(0)(x)=_\mathbb{N}x$ takes a more involved argument and is only true propositionally. Beta-reducing as above produces the term $iter(\mathbb{N},0,succ,x)$ at which point we can't do anything. However, we can use the induction principle for $\mathbb{N}$, i.e. we can use $\mathsf{ind}_\mathbb{N}$, to prove that $iter(\mathbb{N},0,succ,x)=_\mathbb{N}x$ for all $x$. That is, we can produce a term of type $\prod_{x:\mathbb{N}}iter(\mathbb{N},0,succ,x)=_\mathbb{N}x$. We can do that as follows: $$\begin{align}
\mathsf{ind}_\mathbb{N}(& \lambda x:\mathbb{N}.iter(\mathbb{N},0,succ,x)=_\mathbb{N}x, \\ & \mathsf{refl}_0, \\ & 
\lambda n:\mathbb{N}.\lambda p:iter(\mathbb{N},0,succ,n)=_\mathbb{N}n.cong(\mathbb{N},\mathbb{N},iter(\mathbb{N},0,succ,n),n,succ, p))
\end{align}$$
where $cong:\prod_{A:\mathcal{U}}\prod_{B:\mathcal{U}}\prod_{x:A}\prod_{y:A}\prod_{f:A\to B}x =_A y \to f(x) =_B f(y)$ can be defined in using path induction, i.e. $\mathsf{ind}_{=}$ (exercise).
Explicitly writing out the proof term in terms of $\mathsf{ind}_\mathbb{N}$ is probably more formal than the HoTT book intends at that point. (However, one of the key points in the early chapters is justifying [and explaining] the informal notation in terms of the formal terms. So you should be able to work out how these connect.) What the authors would more expect for this example is something like:

Let $C(x)$ be $iter(\mathbb{N},0,succ,x)=_\mathbb{N}x$.
  $\mathsf{refl}_0$ is a value of type $C(0)$ via the first defining
  equation of $iter$. Further for any $n:\mathbb{N}$, given $C(n)$, i.e.
  $iter(\mathbb{N},0,succ,n)=_\mathbb{N}n$, we can produce
  $succ(iter(\mathbb{N},0,succ,n))=_\mathbb{N}succ(n)$ which is
  $iter(\mathbb{N},0,succ,succ(n))=_\mathbb{N}succ(n)$, i.e.
  $C(succ(n))$, via the second defining equation of $iter$. By the
  induction principle for $\mathbb{N}$, this means we have a value of
  $\prod_{x:\mathbb{N}}iter(\mathbb{N},0,succ,x)=_\mathbb{N}x$, i.e.
  $iter(\mathbb{N},0,succ,x)=_\mathbb{N}x$ holds for all $x$.

Your solution to the exercise should look like the above paragraph, except that it will be a statement about a lambda term $rec_\mathbb{N}$ that you will need to explicitly provide. (More ambitiously, you could also have your solution look like the $\mathsf{ind}_\mathbb{N}$ term above.)
I can tell you that it is a bit non-obvious and certainly not trivial (but not that hard) to define $rec_\mathbb{N}$ in terms of $iter$. Indeed, it's trivial to give a lambda term, call it $pred$, such that $pred(succ(n)) = n$ and $pred(0) = 0$ using $rec_\mathbb{N}$, namely $\lambda x:\mathbb{N}.rec_\mathbb{N}(\mathbb{N},0,\lambda n:\mathbb{N}.\lambda y:\mathbb{N}.n,x)$. It's a lot less obvious how to give a lambda term for $pred$ in terms of $iter$.
