With all the excitement about *higher* inductive types (e.g. here and here), it seems worthwhile to work out the theory of conventional (lower?) inductive types in HoTT. That’s what Nicola Gambino, Kristina Sojakova and I have done, as we report in the following paper that’s just been posted on the archive:

The *main theorem* is that in HoTT, what we call the rules for homotopy W-types are equivalent to the existence of homotopy-initial algebras for polynomial functors. The required definitions are as follows:

- the
*rules for homotopy W-types*: the usual rules for W-types of formation, introduction, (dependent) elimination, and computation — but the latter is formulated as a propositional rather than a definitional equality. - a
*weak map of algebras*is a map together with an identity proof , where is the polynomial functor, and a is just a map-algebra , as usual. - an algebra
is *homotopy-initial*if for every algebra, the type of all weak maps is contractible.

So in brief, the extensional situation where “W-type = initial

We focus mainly on W-types because most conventional inductive types like

Of course, the entire development has been formalized in Coq. The files are available in the HoTT repo on GitHub:

There are also some slides (and even a video somewhere) from a talk I recently gave about this at the MAP Workshop, at the Lorentz Center in Leiden. These can be found here.