This posting is the official announcement of The HoTT Book, or more formally:

Homotopy Type Theory: Univalent Foundations of Mathematics
The Univalent Foundations Program, Institute for Advanced Study

The book is the result of an amazing collaboration between virtually everyone involved in the Univalent Foundations Program at the IAS last year.  It contains the state of the art in HoTT as an informal foundation of mathematics, and that requires a bit of explanation.

As readers of this site know, HoTT can be every bit as formal as anyone would like (and more), right down to machine-checkable proofs in Coq and Agda.  But even paper and pencil type theory can be a challenge to understand for the uninitiated — thus the project (proposed by Peter Aczel) of developing some conventions and notation for “informal type theory”. Once the working group at IAS formed, things quickly snowballed from settling on terminology and notation (always a source of healthy dispute!), sample exposition, to writing up some new results in the informal style, and finally an outline of chapters and assignments of authors for first drafts.

Writing a 500 pp. book on an entirely new subject, with 40 authors, in 9 months is already an amazing achievement.  (Andrej Bauer has written a blog post on the sociology of writing the book here — with animation!)  But even more astonishing, in my humble opinion, is the mathematical and logical content: this is an entirely new foundation, starting from scratch and reaching to , the Yoneda lemma, the cumulative hierarchy of sets, and a new constructive treatment of the real numbers — with a whole lot of new and fascinating mathematics and logic along the way. (Mike Shulman has written a blog post with a more detailed outline here.)

But for all that, what is perhaps most remarkable about the book is what is not in it: formalized mathematics.  One of the novel things about HoTT is that it is not just formal logical foundations of mathematics in principle: it really is code that runs in a computer proof assistant.  This book is an exercise in “unformalization” of results that were, for the most part, first developed in a formalized setting.  (Many of the files are available on GitHub and through the Code section of this site.)  At the risk of sounding a bit grandiose, this represents something of a “new paradigm” for mathematics:  fully formal proofs that can be run on the computer to ensure their absolute rigor, accompanied by informal exposition that can focus more on the intuition and examples.  Our goal in this Book has been to provide a first, extended example of this new style of doing mathematics, by developing the latter, informal aspect to the point where — hopefully —others can see how it works and join us in pushing it forward.

To get the book, just go to the Book section of this site and follow the instructions there.

Just some of the authors of The HoTT Book.