Homotopy Type Theory: the book is out!

The long-awaited book on Homotopy Type Theory, a creation of a group of mathematicians working under the collective name of Univalent Foundations Program, is now out! (See here for a snapshot at the content.) And there are many reasons to rejoice:

• I’ve been following with much interest the development of the program, which presents itself as an alternative to set theory for the foundations of mathematics. I don’t expect to understand more than 5% of the mathematical content of the book, but I hope to at least be able to understand the core ideas and have a feel for how they are put in practice.
• It is a fantastic illustration of the power of collective, distributed work in mathematics, which is by and large a discipline still based (at least in theory, if not in practice) on the ‘lone thinker’ model. The book was written in only six months, which would be unthinkable for a single author or even for a small number of co-authors (according to A. Bauer, two dozen mathematicians were involved in the writing process).
• It is entirely and completely open access. What’s more, through the github platform used also in the writing process (which I am myself not familiar with), readers can actively contribute to the content of the book, propose modifications, improvements etc. (Again, my source is Bauer's post.) 

So this new book may rock not only the foundations of mathematics as such; it may also represent a revolution in how mathematics is practiced, a move towards a more collaborative model.

UPDATE: Eric Schliesser has a post at NewAPPS on the book, where he quotes this wonderful passage by Steve Awodey: 

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. 

The philosophical implications of this new approach are (potentially) phenomenal; I hope to be able to say more on the interplay between formalization/unformalization and intuitions in the near future, once I will have had the time to check the book more closely.