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 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 (instead of equivalently ) 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 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 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 “” 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 -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.
,
which is certainly not about adding anything. Part of gets killed, the rest are moved within .
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 -algebra:
is initial if there is a unique homomorphism to any other -algebra
is initial if the slice over , 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 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 corresponds to . Rather, corresponds to . 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.
Nice question! The entry is very confusing, and I think wrong. The reason that is not initial would be that it does not necessarily have the required uniqueness property. But I don’t think that it makes any sense to say that the path object is initial either. The path object is not even precisely defined currently: the properties listed at path space object are somewhat vague. One thing we can note that is that if we have a retraction of the arrow available, such that is homotopic to the identity, then this retraction allows us to construct an algebra morphism from to any up to homotopy. But I don’t see any reason to be able to even construct such a morphism on the nose, never mind the uniqueness property. We can also note that this is not a matter of extensional vs intensional type theory: the best one can hope for is that is isomorphic to the identity, it will never be equal to the identity.
It might be true that, when everything is precisely formulated, one can demonstrate homotopy initiality in some sense. But a) I’d like to see that written down carefully, and b) in that case, since we will have that is homotopy equivalent as an algeba to the path fibration, we would actually be able to take to be initial, and use of the path fibration is somewhat redundant.
Yeah, the page inductive type is wrong as stated. If we refer to an initial object in a 1-category, then we get the diagonal. If we refer to an initial object in an -category, then we get anything equivalent to the diagonal, which includes the path space object but also the diagonal itself. The only way we specifically get the path space object is if we require the inductive type to be a fibration, but in that case it’s not strictly initial any more.
Probably the right thing to do is rework the whole entry to be more precise, and distinguish between syntactic inductive types and their various semantic incarnations.
Nonetheless, the identity type works on a similar setup. I think it’s because we have to require the map X -> A xA to be a fibration in the universal property. A -> A xA is not a fibration, but the universal fix is the path space map A^I -> AxA. There the fibers are Id_A(x, y). I’m actually not sure about this, but my hunch is based on which maps are fibrations in the identity type. Your thoughts?
So (just to be clear) the hunch I have at a fix is that
1) we consider commutative triangles A -> X -> A xA = A -> AxA where X -> AxA is a fibration.
2) a morphism of such diagrams A -> X -> A xA = A -> AxA and A -> Y > A xA = A -> AxA is a fibration X -> Y such that the resulting diagrams commute.
3) A -> A^I -> AxA is initial among such diagrams.
The entry is clearly stubby: its very first line is requesting – since rev 10 from 8 years ago – the syntactic definition to be filled in.
That said, the statement you seem to be discussing is in a section explicitly titled “Semantics” and there moreover after restricting attention to 1-categories.
@Dean: Yes, that’s what I was talking about with ” The only way we specifically get the path space object is if we require the inductive type to be a fibration, but in that case it’s not strictly initial any more.”
Dean, this is discussed in section 2.2 of Schwede 97.
To get spectra, one needs to invert not only itself, but also its action “on finite pointed powers”, in the sense of Prop. 4.7 here.
(This is an abservation due to Goodwillie, follow the pointers behind the above link.)
I think you may be thinking of a different sense of “invert”, Urs. It is true that a pointed -category in which the adjunction is an equivalence is necessarily stable. This is not really “type theory” though, at least not in the sense of HoTT, since pointed and stable -categories do not model HoTT. Although there is now a variant of HoTT that is expected to have models in parametrized spectra and in which is an equivalence for the “stable” objects (the spectra over a point).
Check out the pointer I gave, Prop. 4.7 here, this is about localization in infinity-toposes yielding parametrized spectra.
And it’s exactly what Anel-Finster-Joyal considered.
Right. As I said, that is a different sense of “invert”. Dean’s question asked about and being inverses, not about objects that see them as inverses.
That hair can hardly be split: Once localized. it is what the objects think it is, that’s Yoneda.
If you or Dean feel like providing the precise detail that you would actually like to see discussed, that might make for a more fruitful conversation.
The hair is split by (1) well-typedness, since one question is about a property of a category and the other is about an operation on a category or a subclass of objects, and (2) the fact that the answers are different. I don’t think anyone is saying something should be added to the lab, Dean was just asking a question.
@Mike Shulman: in 29, you’re saying it wouldn’t be inititial with fibrations as maps? Does this mean that the identity type is not unique up to isomorphism, or does it mean we’re missing some property of identity type? Sorry for having to clarify – I’m new to type theory.
By the way, in type theory, I like as a semantics a strict 2-category, which makes things less confusing to me when we have to be rigorous about which things are fibrations in the semantics:
We start with a strict 2-category with objects and . is semantically a map . Context extension is a contravariant functor . We also designate an object in , which we think of as terminal. It sends objects in (which are -cells in ) to objects in . I notate it by , . Dependent sum and dependent product are the same except covariant, and notated and . We also must construct binary pullback and internal hom in each of these categories, and require for , and analogously for internal hom.
To recover the -categorical semantics, let , Let be a certain category , is , is pullback, etc.
In homotopy type theory, is , is the category of infinity groupoids, is a functor, viewing the infinity groupoid as an -category, is , etc.
I think it’s easier to express the path space object in this semantics, since it is clearer how it comes from the identity type.
Yes, in MLTT and Book HoTT the identity type is not unique up to isomorphism. (In cubical type theory, which internalizes an interval object, there is an identity type satisfying a different “path space” universal property that does determine it up to isomorphism.) Note though that this semantic notion of “isomorphism” is not expressible internally (except in a two-level type theory), and the identity type is unique up to the strongest internally-expressible notion of equivalence.
Is it standard, as on this page, to have induction as dependent elimination and recursion as elimination?
Kevin Buzzard is talking about Lean here and seems to split it as recursion is dependent elimination over types, and induction as dependent elimination over propositions.
Isn’t that the more familiar split of recursion as arrow out of initial object and induction as only identity as sub-algebra of initial algebra?
added (here) pointer to the example of the type of Booleans
also deleted (here) the material on the type of natural numbers, since it was nothing but an incomplete early version of the material that has meanwhile been expanded on at natural numbers type. So I left only a pointer to that entry.
tried to polish-up the list of references (here: more bibdata and changes to the ordering for better logic)
also added this pointer:
But I am still looking for a canonical (textbook) reference which would introduce inductive types systematically and comprehensively, i.e. with the inference rules clearly stated and some basic supply of examples actually spelled out.
The textbooks currently listed don’t seem to really live up to this expectation. What are you type theorists pointing your students to when you tell them to learn about inductive types?
Some more edits I made:
moved this item
to W-type, since it seems to barely serve to explain inductive types as such, while at W-type it serves a real purpose
similarly, removed
since this is cited prominently at natural numbers type where the reader will find it following the links provided here
added pointer to:
this is getting closer to what I was hoping to see. Something like this but a tad more expository…
ah, this here looks like it is the origin of the modern notion of inductive types (?):
[ edits: ah, now I see that we have historical comments at Inductive family – history]
The history notes seem to imply that the W-types were introduced in the Padua lectures, but they were already present here. Though published in 1982, that paper was presented on 1979, in this conference.
1 to 53 of 53