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.

This entry was posted in Uncategorized. Bookmark the permalink.

6 Responses to The HoTT Book does not define HoTT

  1. Dan Licata says:

    Seconded!

  2. Steve Awodey says:

    I couldn’t agree more. A huge area that was deliberately omitted was of course semantics, and more generally anything “meta”. Another huge area is the theory of computation, as opposed to mathematics.
    I think the book is best seen as an experiment in one particular aspect og HoTT – to the deliberate exclusion of several others. This is definitely worth pointing out to those who were not involved in writing it.

  3. spitters37 says:

    Great post, Mike. Thanks for clearing that up.

  4. While I suppose that circumstances required writing the above entry, I dearly hope that you, the HoTT community, will be able get back to productive community work and will evade getting bogged down in internal politics, as recent developments seem to suggest there is some danger of. The list of quality contributions here on the blog and on the mailing list, notably by Mike, speak a clear enough language for everyone to see, that letting them speak for themselves might eventually deal with the politics all by itself. Science is not propietary business, and maybe the best way to deal with attempts to make it such is to ignore them and carry on. (Which of course is along the lines of what the above installment says!)

    My wish, if I am allowed to state one: let the next blog installment here be again one of those interesting technical discussions in the overlap of homotopy theory and type theory that make this blog worth reading!

    • Mike Shulman says:

      I’m sorry if I gave the impression that this post was about politics. I really have noticed a number of people who seem to honestly have such misconceptions. The immediate spur to write the post was that a Wikipedia editor was tempted to refer to the book as “establishing” the field, but I have the feeling that I’ve fielded similar misconceptions from people on stackexchange and/or mailing lists before. No blame to any of them! I think that (in hindsight) it’s actually a fairly natural thing to think, for newcomers whose primary exposure to the subject is through the book.

  5. How may HoTT be applied to computing? Could a HoTT-derived type system be useful for programming languages?

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s