Since spring, and even before that, I have participated in a
great collaborative effort to write a book on homotopy type theory.
It is finally finished and ready for public consumption. You can
get the book freely at http://homotopytypetheory.org...