I have added to *inductive type* in the *Examples section* the missing subsection *Path recursion* to go with the section *Path induction* that was there before.

It’s a mistake to say that $0$ corresponds to $1 +$. Rather, $0$ corresponds to $1$. The $+$ is different. This may make it harder to mix things up. Otherwise I agree with Mike #14.

]]>Yes, that’s right. And it’s important in type theory, for the reasons you mention. The “standard” elimination can also be called *dependent* elimination for clarity (since the type being eliminated into may depend on $W$ itself). The really nifty thing, I think, is that dependent elimination gives us a (homotopy) initial algebra, in particular a *unique* morphism into any other algebra, without our having to explicitly assert any uniqueness (and in particular without referring explicitly to any notion of “equality”).

Coming back to the point discussed at the beginning of this thread here, that there are these two equivalent formulations of initial $F$-algebra:

$W$ is initial if there is a unique homomorphism to any other $F$-algebra

$W$ is initial if the slice over $W$, as algebras, is pointed

There is a deeper duality to this, right? The second is what is *induction* as such, whereas the first is *recursion*.

Since it’s equivalent, it may seem strange to make the distinction. But it is true that the induction principle *verbatim* as traditionally stated comes out with the second definition.

In Awodey-Gambino-Sojakova (but probably not just there) I see this distinction made around page 9. Also with different names for the type theory rules: *simple elimination* in the first case as opposed to the standard *elimination* in the second.

I am just saying this to check if I am missing something. If not, I will work some remarks along these lines into the entry.

]]>Ah, I see. Thanks.

]]>Just Hilbert’s hotel, no?

You can better get used to avoiding the +1 trap, by turning things about and thinking about coalgebras.

$X \to 1 + X$,

which is certainly not about adding anything. Part of $X$ gets killed, the rest are moved within $X$.

]]>The “1+” is related to the 0, not the successor. If you want to say “The natural numbers are the universal thing that does not change when you add one component” then you can think about taking the whole natural numbers and shifting them up one in order to “add one component” at the *bottom*, namely 0. (I’m actually not sure how you could “add one component” to the “top” of the natural numbers and leave it unchanged…)

I have spelled out at *inductive type* in the section *Examples - Natural numbers* (scroll down to what currently is “Example 1”) a detailed walk through how the induction principle works for an $\mathbb{N}$-dependent proposition, in terms of the categorical semantics of elimination and computation rules.

I am working on prettifying and expanding *inductive type* (didn’t get very far yet, though).

Here is one dumb little question on the most basic of all examples. I nevertheless have this question at the moment:

when we write the endofunctor whose initial algebra is the natural numbers object as $F(X) = 1+ X$ (instead of equivalently $F(X) = * \coprod X$) it *looks* very nicely suggestive: by Lambek’s theorem the natural numbers are a fixed point of this functor, and so it seems suggestive to read $F(X) = 1 + X$ as saying “The natural numbers are the universal thing that does not change when you add one component.”

Nice. But then, when one looks at how an inital algebra for this $F$ gives a natural number object, it is *not* the “1”-summand above that induces the successor function. The 1-summand induces the 0-element

Sorry for this stupidity, but do you see what I am wondering about? On the one hand the “1+” in “$1+ X$” seems related to the successor, in the other to the 0.

How should I think about this, morally?

]]>Thank you, Mike! This looks very useful.

]]>I have added to inductive type a link to a recent paper on the arXiv about homotopy-initiality of inductive types in homotopy type theory. See also a HoTT blog post.

]]>Yes, this I like! Thanks.

]]>Okay, I got rid of this phrase. I’ll suppose it now reads okay unless you tell me otherwise.

]]>I don’t find “As a reality check” to be a useful phrase. Why not say explicitly “Let’s check that indeed if … then …”?

But if you don’t like it, I won’t object further.

]]>Urs #5: okay, I see what you’re saying. Does it read better now than it did?

]]>the point is to check that we get the usual notion of initial algebra on the nose in the case where equality is extensional.

Yes, and this is what my sentence tries to say explicitly. When I first read your “as a reality check” I was confused about what it is you were going to check.

If my sentence doesn’t cut it, replace it by another one. But I think it helps the reader to say in advance which reality it is that is going to be checked.

]]>Actually, I liked the way I had it (“as a reality check”, etc.). Those particular words are not so important, but the point is to check that we get the usual notion of initial algebra on the nose in the case where equality is extensional. Yes, this might be considered trivial, but it’s good pedagogy for readers who have spent most of their lives thinking of equality as extensional, and IMO we should be very gentle in easing people into intensional type theory or homotopy type theory (as I can attest, being someone who has found this material very hard to follow).

The comments Mike added to the page (thanks, Mike!) then lead naturally to the meaning of the words “essentially unique” (unique up to contractible space of choices).

]]>Thanks, this is great! I added a few more comments.

]]>I have taken the liberty to replace the four words “As a reality check” with the sentence: “Notice that these axioms still imply that algebra maps out of $W$ are essentially unique, even though that is not stated explicitly. ” Hope that’s okay.

Also I have added some hyperlinks.

]]>Based on a private discussion with Mike Shulman, I have added some explanatory material to inductive type. This however should be checked. I have created an opening for someone to add a precise type-theoretic definition, or I may get to this myself if there are no takers soon.

]]>