The n-Category Café

I intend this to be my last effort at popularization of HoTT for some time, and accordingly it ended up being rather comprehensive. It begins with a 20-page introduction to type theory, from the perspective of a mathematician wanting to use it as an internal language for categories. There are many introductions to type theory, but probably not enough from this point of view, and moreover most popularizations of type theory are rather vague about its categorical semantics; thus I chose (with some additional prompting from the editors) to spend quite some time on this, and be fairly (though not completely) precise about exactly how the categorical semantics of type theory works.

I also decided to emphasize the point of view that type theory (and “syntax” more generally) is a presentation of the initial object in some category of structured categories. Some category theorists respond to this by saying essentially “what good is it to describe that initial object in some complicated way, rather than just studying it categorically?” It’s taken me a while to be able to express the answer in a really satisfying way (at least, one that satisfies me), and I tried to do so here. The short version is that by explicitly constructing an object that has some universal property, we may learn more about it than we can conclude from the mere statement of its universal property. This is one of the reasons that topologists study classifying spaces, category theorists study classifying toposes, and algebraists study free groups. For a longer answer, read the chapter.

After this introduction to ordinary type theory, but before moving on to homotopy type theory, I spent a while on synthetic topology: type theory treated as an internal language for a category of spaces (actual space-spaces, not $\infty$-groupoids). This seemed appropriate since the book is about all different kinds of space. It also provides a good justification of type theory’s constructive logic for a classical mathematician, since classical principles like the law of excluded middle and the axiom of choice are simply false in categories of spaces (e.g. a continuous surjection generally fails to have a continuous section).

I also introduced some specific toposes of spaces, such as Johnstone’s topological topos and the toposes of continuous sets and smooth sets. I also mentioned their “local” or “cohesive” nature, and how it can be regarded as explaining why so many objects in mathematics come “naturally” with topological structure. Namely, because mathematics can be done in type theory, and thereby interpreted in any topos, any mathematical construction can be interpreted in a topos of spaces; and since the forgetful functor from a local/cohesive topos preserves most categorical operations, in most cases the “underlying set” of such an interpretation is what we would get by performing the same construction directly with sets. This also tell us in what circumstances we should expect a construction that takes account of topology to disagree with its analogue for discrete sets, and in what circumstances we should expect a set-theoretic construction to inherit a nontrivial topology even when there is no topological input; read the chapter for details.

The subsequent introduction to homotopy type theory and synthetic homotopy theory has nothing particularly special about it, although I decided to downplay the role of “fibration categories” in favor of $(\infty,1)$-categories when talking about higher-categorical semantics. Current technology for constructing higher-categorical interpretations of type theory uses fibration categories, but I don’t regard that as necessarily essential, and future technology may move away from it. In particular, in addition to the intuition of identity types as path objects in a model category, I think it’s valuable to have a similar intution for identity types as diagonal morphisms in an $(\infty,1)$-category.

The last section brings everything together by discussing cohesive homotopy type theory, which is of course one of my current personal interests, modeling the local/cohesive structure of an $(\infty,1)$-topos with modalities inside homotopy type theory. As I’ve said before, I feel that this perspective greatly clarifies the distinction and relationship between space-spaces and $\infty$-groupoid “spaces”, with the connecting “fundamental $\infty$-groupoid” functor characterized by a simple universal property.

Finally, in the conclusion I at last allowed myself some philosophical rein to speculate about synthetic theories as foundations for mathematics, as opposed to simply internal languages for categories constructed in an ambient classical mathematics. Once we see that mathematics can be formulated in type theory to apply equally well in a category of spaces as in the category of sets, there is no particular reason to regard the category of sets as the “true” foundation and the category of spaces as “less foundational”. Just as we can construct a category of spaces from a category of sets by equipping sets with topological structure, we can construct a “category of sets” (i.e. a Boolean topos) from a “category of spaces” by restricting to the subcategory of objects with uninteresting topology (the discrete or codiscrete ones). Either category, therefore, can serve as an equally valid “reference frame” from which to describe mathematics.