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 -algebra is just a map , 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.