Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.
Thanks, this is great! I added a few more comments.
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).
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.
Urs #5: okay, I see what you’re saying. Does it read better now than it did?
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.
Okay, I got rid of this phrase. I’ll suppose it now reads okay unless you tell me otherwise.
Yes, this I like! Thanks.
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.
Thank you, Mike! This looks very useful.
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
$(zero, successor) : * \coprod X \to X \,.$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?
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.
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…)
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$.
Ah, I see. Thanks.
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.
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”).
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.
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.
1 to 20 of 20