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 -algebra” now becomes “homotopy W-type = homotopy-initial -algebra”. Perhaps not very surprising, once one finds the right concepts; but satisfying nonetheless.
We focus mainly on W-types because most conventional inductive types like can be reduced to these; in fact, the possibility of such reductions is itself part of our investigation. There are some results in extensional type theory (cited in the paper) showing that many inductive types are reducible to W-types, and there is some literature (also cited) showing how such reductions can fail in the purely intensional theory. We show that in HoTT some of these reductions go through, provided both the W-types and the inductive types are understood in the appropriate “homotopical” way, with propositional computation rules. The detailed investigation of more such reductions is left as future work.
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.