2
$\begingroup$

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 ?

$\endgroup$
  • $\begingroup$ 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 $\endgroup$ – elidiot May 4 '19 at 19:27
  • $\begingroup$ @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) $\endgroup$ – Maxime Ramzi May 5 '19 at 10:20
  • $\begingroup$ BTW, your version of the recursor is also called the iterator. See exercise 1.4 in the HoTT Book. $\endgroup$ – Mike Shulman May 5 '19 at 21:24
  • $\begingroup$ @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 ! $\endgroup$ – Maxime Ramzi May 5 '19 at 21:34
3
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ If I understand correctly the discussion there, you were trying to see if recursion implies induction, but that's not really my question here; or if it is I can't see how ? $\endgroup$ – Maxime Ramzi May 4 '19 at 21:06
  • $\begingroup$ That was not explicit in my message, but if you look more closely at the example that was given, it shows that both the recursion and induction principles can be derived from a more simple principle that is the one that you are proposing. $\endgroup$ – L. Garde May 4 '19 at 21:15
  • $\begingroup$ More precisely: by applying the simple principle to the product of N x C, you can derive the recursion principle; by applying it to the dependant product Exists (x:N) C(x), you can derive the induction principle. $\endgroup$ – L. Garde May 4 '19 at 21:21
  • $\begingroup$ 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 ? $\endgroup$ – Maxime Ramzi May 4 '19 at 21:30
  • 1
    $\begingroup$ 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. $\endgroup$ – L. Garde May 5 '19 at 6:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.