Fixed typos in the term elimination and computation rules for the natural numbers.

]]>Thanks for the hint! I have added the reference, here and also at *W-type* (as announced there)

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.

]]>added the induction rule for the empty type to the list of Examples (here), typeset so as to fit the pattern of the following rules

]]>Under “Examples – Unit type” (here) I have added the inductive inference rules for the unit type

]]>added list of references on categorical semantics (here)

]]>compiled these and related original references into a References-subsection “History of inductive types” (now here)

cf. forum discussion here

]]>ah, this here looks like it is the origin of the modern notion of inductive types (?):

- Thierry Coquand, Christine Paulin,
*Inductively defined types*, Lecture Notes in Computer Science**417**, Springer (1990) [doi:10.1007/3-540-52335-9_47]

[ edits: ah, now I see that we have historical comments at *Inductive family – history*]

added pointer to:

- Paul Francis Mendler,
*Inductive Definition in Type Theory*, Cornell (1987) [hdl:1813/6710]

this is getting closer to what I was hoping to see. Something like this but a tad more expository…

]]>tried to polish-up the list of references (here: more bibdata and changes to the ordering for better logic)

also added this pointer:

- Simon Thompson, §4.10 in:
*Type Theory and Functional Programming*, Addison-Wesley (1991) [ISBN:0-201-41667-0, webpage, pdf]

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

- Michael Abbott, Thorsten Altenkirch, Neil Ghani,
*Inductive Types for Free – Representing nested inductive types using W-types*, talk at ICALP (2004) [pdf]

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

- Frank Pfenning,
*Lecture notes on natural numbers*(2009) (pdf)

since this is cited prominently at *natural numbers type* where the reader will find it following the links provided here

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.

Added some text about nat and lists moved from W-type.

]]>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?

]]>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.

]]>@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 $U$ with objects $*$ and $\text{Type}$. $C : \text{Type}$ is semantically a map $* \rightarrow \text{Type}$. Context extension is a contravariant functor $[*, \text{Type} ] \rightarrow U$. We also designate an object $\star$ in $[*, \text{Type}]$, which we think of as terminal. It sends objects $* \rightarrow \text{Type}$ in $[*, \text{Type}]$ (which are $1$-cells in $U$) to objects in $U$. I notate it by $X \mapsto [-, \text{Type}]$, $(f : X \implies Y) \mapsto f_* : [Y, \text{Type}] \rightarrow [X, \text{Type}]$. Dependent sum and dependent product are the same except covariant, and notated $f^*$ and $f^!$. We also must construct binary pullback and internal hom in each of these categories, and require $f^! f_* Y = X \times Y$ for $f : X \implies *$, and analogously for internal hom.

To recover the $1$-categorical semantics, let $U = \text{Cat}$, Let $\text{Type}$ be a certain category $C$, $[X, C]$ is $C/X$, $f_*$ is pullback, etc.

In homotopy type theory, $U$ is $(\infty, 1)-\text{Cat}$, $\text{Type}$ is the category of infinity groupoids, $[X, C]$ is a functor, viewing the infinity groupoid $X$ as an $(\infty, 1)$-category, $f_*$ is $[f, C]$, 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.

]]>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.

]]>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.

]]>Right. As I said, that is a different sense of “invert”. Dean’s question asked about $\Sigma$ and $\Omega$ *being* inverses, not about objects that *see them as* inverses.

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.

]]>I think you may be thinking of a different sense of “invert”, Urs. It is true that a pointed $(\infty,1)$-category in which the adjunction $\Sigma \dashv \Omega$ 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 $(\infty,1)$-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 $\Sigma\dashv\Omega$ is an equivalence for the “stable” objects (the spectra over a point).

To get spectra, one needs to invert not only $\Sigma \Omega$ 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.)

]]>Dean, this is discussed in section 2.2 of Schwede 97.

]]>Probably you know the answer to this. ]]>