The HoTT Book does not define HoTT

The HoTT Book does not define HoTT

The intent of this post is to address certain misconceptions that I’ve noticed regarding the HoTT Book and its role in relation to HoTT. (At least, I consider them misconceptions.) Overall, I think the HoTT Book project has been successful beyond the dreams of the authors, both in disseminating the ideas of the subject to a wide audience, and in serving as a reference for further work. But perhaps because of that very success, it’s easy for people to get the impression that the HoTT Book defines the field in some way, or that its particular conventions are universal.

In fact, this is not at all the case, nor was it the intention of the authors. (At least, it was never my intention, and I didn’t get the impression that any of the other authors felt that way either.) Many aspects of the book are particular to the book, and should not be regarded as circumscribing or limiting the subject, and especially not as excluding anything from it. Below I will mention three particular examples of this, but there may be others (feel free to discuss in the comments).

Example (1): the book is only about one particular aspect of the subject, namely doing informal mathematics internally to HoTT. Moreover, even within this aspect, the book only scratches the surface. It focuses particularly on on what is new about doing math this way (e.g. synthetic homotopy theory and the advantages of HITs). But homotopy type theory as a subject also includes many other things, such as very ordinary classical mathematics, computer formalization, higher-categorical semantics, oo-groupoid structures on types, etc.

Example (2): by necessity, the book uses one particular type system. The type system we chose happens to have e.g. judgmental eta for functions, HITs with judgmental computation for point-constructors but not path-constructors, a tower of cumulative Russell universes indexed by an external nat, and so on. But plenty of other type systems — old, new, and yet to be invented — can also be used for “doing HoTT”. Vladimir has proposed a type system HTS that internalizes strict equality; I’d like to try type systems with infinitary constructors; we may eventually need to weaken aspects of the type theory to match desired semantics; some models for HITs suggest that there may be ways to make the path-constructors judgmental; Francois has suggested different ways to treat universes; a fully constructive version of univalence might involve recursively defined path-types rather than inductively generated ones; and so on.

Example (3): for reasons adumbrated in section 3.10, the book allows any type to be treated as a “proposition”, and inserts the adverb “merely” for (-1)-truncatedness. But as should be clear from the reasons given in 3.10, this is in no way a necessary choice; it was among other things an experiment. Plenty of people prefer to make a different choice, and they are still “doing HoTT”. Personally, I wish that someone would try forking the book and rewriting it using the other convention that only (-1)-truncated types can be propositions; then we could compare the two for ease and readability.

In summary, homotopy type theory is still a very young field, with lots of ideas to explore, plenty of which we haven’t even thought of yet. It’s much too early to standardize. The HoTT Book is great, but let’s not be limited by it.