The n-Category Café

So where did this book come from? As it says in the preface, we did not set out to write a book. It all began last fall when Peter Aczel proposed to start a working group on informal type theory. I’ve mentioned this idea before: the point is that type theory is usually a very formalized system (even to the point of being implemented in computer proof assistants), whereas mathematicians are accustomed to speak instead in informal “mathematical English” (or French, Russian, etc.). The usual implicit assumption is that mathematical English could be formalized in a set-theoretic foundation such as ZFC, and this requires various conventions on what we can and can’t say in mathematical English. The goal of informal type theory is to develop conventions for a version of mathematical English whose “implicit underlying foundation” is instead type theory — specifically, homotopy type theory.

The informal type theory working group met a few times and had some good arguments, but after a while we realized we needed something to focus our discussions. So we began a project of writing down some of our recent results in homotopy type theory in informal mathematical English, and to give the project some coherence (and an incentive to settle on uniform conventions) we thought of what we were writing as chapters in a book. Eventually we noticed that an actual book was starting to take shape, and that such a book could be extremely valuable, both as a “report” on the progress of the special year, and as an introduction for newcomers to the field not requiring them to know or learn any formalized type theory. Hence, the HoTT Book.

Due to its origins, some of the material in the book has already been published elsewhere, while some of it was “common knowledge” in the HoTT community before the IAS program but may not have been written down anywhere (except perhaps in a computer proof assistant). On the other hand, a good amount of the material is new, and may yet be published elsewhere by the people responsible for it (or, in a couple of cases, was published elsewhere during the writing of the book). Making the latter possible is one reason we chose a permissive license.

I want to emphasize that the book is specifically intended to be readable by mathematicians who do not know any type theory, any computer science — or even any homotopy theory! If you are reading this blog, chances are you are in the intended audience. So you should go have a look!

That said, type theory can be very difficult to explain to a mathematical audience. We did our best to give a “working mathematician’s” introduction to type theory in the first couple of chapters of the book, but I am certain that for many readers, it will still be confusing. We want your feedback! We will be releasing “bug fix” enhancements on a rolling basis based on reader feedback, and eventually there may be an official Second Edition. Tell us what is confusing, where you got lost, where there are typos, where the math is just wrong, etc. etc. We’d prefer if you open a github issue on the book project, but it’s also fine to just put a comment on the HoTT blog. And of course we’re very happy to discuss what’s in the book as well.

To whet your appetite, I will end this post with an annotated table of contents of the book.

1. Type theory. This chapter is a brief introduction to dependent type theory without any homotopical features. It begins with an overview of how type theory differs from set theory as a foundation for mathematics (influenced by discussions such as this and this), and then introduces concepts like type universes, dependent types (which in the book we call type families), $\lambda$-abstraction, induction and recursion, and propositions-as-types. It also establishes notation and conventions for the rest of the book.

2. Homotopy type theory. This chapter introduces the homotopical viewpoint on type theory, where “proofs of equality” are regarded as paths in a space or equivalences in an $\infty$-groupoid. It also adds to type theory the function extensionality and univalence axioms — of which the latter, due to Voevodsky, is one of the main innovations of homotopy type theory. Finally, it explains how to “compute” with paths in various kinds of types, and proves that many types have universal properties.

3. Sets and logic. This chapter begins by defining a class of types called sets, which have no “higher homotopy” and hence behave basically like the sets in a (structural) set theory such as ETCS. Then it discusses various aspects of logic in homotopy type theory, introducing “mere propositions” ($(-1)$-truncated types) and the corresponding propositional truncation, and statements of the law of excluded middle, the axiom of choice, and the propositional resizing axiom (none of which we need to use very much in the rest of the book).

4. Equivalences. This chapter studies several equivalent ways to define the notion of “equivalence of types” in a well-behaved way. It also proves some useful general facts about equivalences, and that the univalence axiom implies the function extensionality axiom.

5. Induction. This chapter adds to our type theory the general notion of inductive type, which includes most of the type forming operations from chapter 1 as special cases. It proves (by a sufficiently general example, namely Martin-Löf’s $W$-types) that inductive types can equivalently be characterized as homotopy-initial algebras for polynomial endofunctors, and describes briefly several generalizations of inductive types such as inductive families, inductive-inductive types, and inductive-recursive types.

6. Higher inductive types. Next to univalence, HITs are the most important new aspect of homotopy type theory, allowing us to construct higher-dimensional “spaces” such as spheres and tori; perform homotopical constructions such as suspensions, truncations, localizations, and homotopy colimits; and generate free algebraic structures of all sorts. This chapter introduces them by way of many examples.

7. Homotopy $n$-types. This chapter studies the general notion of $n$-type, which includes sets (0-types), mere propositions ($(-1)$-types), and contractible types ($(-2)$-types) as special cases. It defines the $n$-truncation operation using higher inductive types, and constructs the ($n$-connected, $n$-truncated) orthogonal factorization system on types. It ends with a brief discussion of more general “modalities”.

8. Homotopy theory. Here we finally start to get the payoff. Combining higher inductive types with univalence, we calculate $\pi_1(S^1)$, $\pi_n(S^n)$, and $\pi_3(S^2)$, construct long exact sequences and the Hopf fibration, and prove the Freudenthal suspension theorem and the van Kampen theorem. We also prove that Whitehead’s theorem holds for $n$-types for any finite $n$, and observe that its general form can be regarded as a foundational axiom (“Whitehead’s principle”) akin to excluded middle or choice. This chapter incorporates a lot of new work that was done this past winter and spring.

9. Category theory. I blogged about the contents of this chapter already. The basic idea is that if we define “categories” appropriately, requiring them to satisfy a “local” version of the univalence axiom, then all proofs and constructions will automatically be invariant under isomorphism of objects in a category and under equivalence of categories. In particular, equivalent categories become equal.

10. Set theory. This chapter begins by proving that the “sets” (as defined in chapter 3) do in fact satisfy the axioms of ETCS (or a constructive version thereof, depending on whether we assume excluded middle and choice). Then it studies a few topics from traditional “set theory”, such as cardinal and ordinal numbers, finding that they behave mostly like their classical versions, but are slightly improved by univalence. Finally, it constructs a model of ZF-style set theory inside homotopy type theory, using a higher inductive type to model the cumulative hierarchy.

11. Real numbers. This chapter explores two definitions of the real numbers. First there are the Dedekind reals, which behave just as expected (modulo issues of constructivity and predicativity). Then there are the Cauchy reals, for which we can use a higher inductive-inductive type to improve on the usual constructive treatment. If we assume excluded middle, then both definitions agree and behave like the real numbers we are all familiar with. It ends by sketching another higher inductive-inductive definition: Conway’s surreal numbers.

For more blogging about the HoTT Book, see the official announcement post by Steve Awodey, which discusses the paradigm of “unformalization”, and this post by Andrej Bauer, which discusses the socio-technological aspects of writing the book (which was a new and fascinating experience).