The HoTT book defines $\mathbb{N}$ to have $0:\mathbb{N}, succ: \mathbb{N\to N}$ and a recursion constructor $\prod_{C:\mathcal{U}}C\to (\mathbb{N}\to C\to C)\to \mathbb{N}\to C$ with a certain defining relation.
I'm wondering why the constructor is not more simply defined as a term $rec:\prod_{C:\mathcal{U}}C\to (C\to C)\to \mathbb{N}\to C$ with defining relations $rec(C,c_0,f,succ(n)) \equiv f(rec(C,c_0,f,n))$ and $rec(C,c_0,f,0) \equiv c_0$ ?
Indeed that recursion type would correspond to $\mathbb{N}$ being an "NNO" (natural numbers object) by analogy with a topos for instance; and the one given by the HoTT book seems equivalent by currying :
Indeed we can define a term $Hrec : \prod_{C:\mathcal{U}}C\to (\mathbb{N}\to C\to C)\to \mathbb{N}\to C$ as $\lambda C:\mathcal{U}. \lambda c_0: C. \lambda c_s: (\mathbb{N}\to C\to C).\lambda n : \mathbb{N}. pr_2(rec(\mathbb{N}\times C, (0,c_0),H(c_s),n)) $ where $H(c_s) :\equiv \lambda n:\mathbb{N}.\lambda x:C. (succ(n),c_s(n)(x))$.
What I'm saying is just that the recursion they define seems to be a special case of the one I propose (of course the converse is also true); and that mine seems way simpler in its definition.
While writing a proof that the defining equations the HoTT book gives for their $rec$ were satisfied by my $Hrec$, I realized that I used $x \equiv (pr_1(x),pr_2(x))$ for $x:A\times B$, which isn't true : we "only" have $uniq_{A\times B} : x=(pr_1(x),pr_2(x))$ and so my constructor doesn't actually allow to define the one in HoTT (or at least it doesn't seem to allow that), although there is probably a term $p: Hrec(blabla) = rec_{HoTT}(blabla)$ : is that the case ?
Am I right in thinking that the reason I just gave is the one why the HoTT book didn't go with my "simpler looking" recursion operator ?
But in that case, why assume we have this stronger one ? And why not go further, like have $u_{n+1}$ depend on $n,u_n$ and all the $u_k$'s below, or I don't know, something that wouldn't be judgmentally equal either but that would be stronger ? Indeed, classically, most, if not all ($\mathbb{N}$-)recursion principles derive from the one I gave, even the more sophisticated-looking ones, so why give this specific one ?
( a question that might be more complicated to answer and even formalize is : is there a way to prove that my recursion operator doesn't allow us to build the one from the HoTT book ?)
EDIT : I just realized that the recursion operator proposed in HoTT makes way more sense if we want to allow an induction operator to allow for dependent types. That is, if we have a dependent type $C:\mathbb{N}\to \mathcal{U}$, we can't just afford to have "$f:C\to C$" because it doesn't make sense, we have to have something like "$f_n:C(n)\to C(succ(n))$" and so there has to be a dependency in $n$ : hence $\mathbb{N}\to C\to C$ instead of $C\to C$. Is it the actual reason ?
Best Answer
I asked a very similar question last year on the Hott Cafe forum: https://groups.google.com/forum/#!topic/hott-cafe/PQe7SI3nwcE
The answer is that the induction principle can indeed be derived from the recursion principle, however only if you have a judgemental eta rule for the recursor, which is not the case in the HoTT book.