# Why such a complicated definition of recursion for $\mathbb{N}$ in HoTT?

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 ?

• I think I understood your problem. With the language of the section 5.4 of the HoTT book, we can see your version of $\mathbb N$ as an $\mathbb N$-algebra. If we try to show that it is initial (which would imply that it is equal to their $\mathbb N$), we have to use the induction principle of their $\mathbb N$ to show the contractibility. Would you also want to change the induction principle ? In that case this could be more complicated May 4, 2019 at 19:27
• @DerekElkins well, anything that's awkward to define with $rec$ is awkward with the first form if my proposed $Hrec$ actually worked (again, classically, it is very easy to reduce any form of recursion to my simple recursion - here the issue seems to be related to judgmental vs propositional equality) May 5, 2019 at 10:20
• BTW, your version of the recursor is also called the iterator. See exercise 1.4 in the HoTT Book. May 5, 2019 at 21:24
• @MikeShulman : for some reason I haven't seen that yet, thanks for pointing it out. Btw, if you have anything to add to the existing answer, I'd be glad to hear what you have to say ! May 5, 2019 at 21:34

• Oh alright, I didn't see that, ok, thank you ! But so if I understand correctly, for this to work, you have to have a judgmental $\eta$ rule ? And also, does the simple principle actually imply the recursion principle, isn't there a problem with "$x=(pr_1(x), pr_2(x))$" not being a judgmental equality ? May 4, 2019 at 21:30
• Yes, you need judgmental $eta$ rule. Taking your example, you then need that pr1(rec(NxC,(0,c_0),H(c_s),n) = rec(N,0,succ(n),n) = n and the recursion principle can then be derived using pr2. May 5, 2019 at 6:41