Pretty big book news (in a couple of ways)! The Univalent Foundations Program at the Institute for Advanced Study in Princeton has released a 470-page textbook resetting the foundations of mathematics on homotopy type theory. It’s called Homotopy Type Theory: Univalent Foundations of Mathematics.
This book is so fashionable it hurts: 40 authors collaborated on GitHub to produce a 470-page Creative Commons-licensed book in six months, without the involvement of any academic publisher. The book resets the foundations of mathematics in terms that suit computer formalisation – they formalised their theory in both Coq and Agda before writing the book. Several of the authors are active on Google+ answering questions about it. Even the formatting of the book is modern – citations in the text link to references in the bibliography, and references in the bibliography link back to citations in the text. The only thing that could’ve put it even more on-trend would be if it all fitted into a single tweet. It’s certainly no heavier than it needs to be, though: while Principia Mathematica famously took 379 pages to prove $1+1=2$, Homotopy Type Theory gets from explaining the basics of type theory to computing the higher homotopy groups of spheres in the first 250 pages.
So what’s the big deal, mathematically? The back cover of the book puts it quite well:
Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. It touches on topics as seemingly distant as the homotopy groups of spheres, the algorithms for type checking, and the definition of weak ∞-groupoids.
Homotopy type theory brings new ideas into the very foundation of mathematics. On the one hand, there is Voevodsky’s subtle and beautiful univalence axiom. The univalence axiom implies, in particular, that isomorphic structures can be identified, a principle that mathematicians have been happily using on workdays, despite its incompatibility with the “official” doctrines of conventional foundations. On the other hand, we have higher inductive types, which provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory: spheres, cylinders, truncations, localizations, etc. Both ideas are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of “logic of homotopy types”.
This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an “invariant” conception of the objects of mathematics — and convenient machine implementations, which can serve as a practical aid to the working mathematician. This is the Univalent Foundations program.
The present book is intended as a first systematic exposition of the basics of univalent foundations, and a collection of examples of this new style of reasoning — but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant. We believe that univalent foundations will eventually become a viable alternative to set theory as the “implicit foundation” for the unformalized mathematics done by most mathematicians.
In brief, this is another step in the quest to unify all mathematics on consistent foundations. You could say that that project began with the axiomatisation of geometry leading to Euclid’s Elements, and really got going at the start of the 20th century with Russell and Whitehead’s Principia Mathematica, which tried to state everything in terms of sets. Set theory had a huge paradox in the middle of it, so mathematicians have spent the time since Principia trying to come up with something that puts it all on a firm footing. Bourbaki restates all of maths in terms of Zermelo-Fraenkel set theory with the axiom of choice, but some people have serious objections to that too. Meanwhile, category theory and model theory have been providing as much abstraction as anyone can usefully apply, and the advent of computer proof has made constructivism, where you can only accept something exists once you’ve explicitly constructed it, much more popular.
Homotopy type theory unifies type theory, arising from logic and computer science, with homotopy theory, which talks about topological spaces. In classical set theory, the base objects are sets, and propositions about those sets exist elsewhere. In homotopy type theory, objects and propositions about objects are instances of the same kind of thing – types – and you can think of types as being spaces of points, which is where the homotopy theory comes in. The philosophy of the book is generously constructivist – they avoid non-constructive concepts like the axiom of choice or law of the excluded middle right up until they need them for things like defining the real numbers.
Like Bourbaki, the presentation of these ideas is just as important as the ideas themselves, and the book delivers on that too. The authors have learnt the lesson of Russell and Whitehead, and use notation deftly to avoid losing the reader in a morass of symbols. The introductory sections are short and to the point, giving definitions and justification concisely and clearly. The language is approachable and not at all high-falutin’.
That’s about as far as I can go explaining the book before I say something completely stupid, so it’s fortunate that there has been a proliferation of blogging and commenting by the authors to explain the book in the couple of days since it was released.
- The HoTT blog has a post by Steve Awodey announcing the book.
- Andrej Bauer announced the release of the book on Google+ with a bold claim: “Today is the last day of the reign of set theory. Now that I got your attention: the Homotopy Type Theory Book is out!
- Andrej posted about the process of writing the book and the reasons for its completely open release.
- Carlo Angiuli has written an “introduction to the introduction”, explaining very clearly to the (relative) layman what’s going on.
- Mike Shulman has posted on the n-Category Café about the origins of the book and gives an ‘annotated table of contents’.
- John Baez posted on Google+ about the book, and an informative questions-and-answers session has arisen in the comments.
Andrej Bauer produced this video showing the contributions of the authors on the source TeX files while the book was being written:
[vimeo url=https://vimeo.com/68761218]
Finally, I can’t allow this reference spotted by Chandan Dalawat in the Bibliography to pass without comment:
[EucBC] Euclid. Elements, Vols. 1–13. Elsevier, 300 BC. (Cited on page 57.)
Cheeky!
Links
Download the book or buy a physical copy.
Official blog post announcing the book.
The goals of the original Univalent Foundations of Mathematics program at the Institute for Advanced Study.
Two minor technical corrections, if I may.
Principia Mathematica did not use sets but rather types. Russell invented type theory, although today we do not use it in his original form. Sets in modern form came later, I think as a simplification of Russell’s type theory. Also, the paradoxes you speak about were eliminated by Russell, and that was in fact the main motivation for him inventing types, he wanted to get rid of the pardoxes in Frege’s system.
Second, in the HoTT book we do not need choice or excluded middle for real numbers. All constructions of reals are constructive and avoid choice. The place where choice and excluded middle are used most blatantly is in the chapter on sets, sections on cardinals and ordinals. There is no way around that, since constructive ordinals ae weird, and the constructive cardinals not very useful. I think everywhere else we pretty much avoid choice and excluded middle, except to show how it influences things. For example, with excluded middle the closed interval is compact, but without it we first have to fix the usual definition of cover, which complicates things a bit.