[Agda] The HoTT book

[Andrej Bauer]

Dear all,

I am very happy to announce the first public release of the "HoTT Book":

Homotopy Type Theory: Univalent Foundations of Mathematics

by Univalent Foundations Project
at Institute for Advanced Study

The book is freely available at http://homotopytypetheory.org/book/

You can download PDF in several formats, or cheaply buy a bound copy.

There are by now several blog posts about the book which explain well
what it is about:

* the official announcement by Steve Awodey:
http://homotopytypetheory.org/2013/06/20/the-hott-book/
* Mike Shulman's announcement on n-Cafe:
http://golem.ph.utexas.edu/category/2013/06/the_hott_book.htmlhttp://golem.ph.utexas.edu/category/2013/06/the_hott_book.html
* Andrej Bauer discusses the social and technological aspects of
writing the book at http://audrey.fmf.uni-lj.si/hott.html
* Bob Harper announces the book and discusses what needs to be done:
http://existentialtype.wordpress.com/2013/06/20/the-homotopy-type-theory-book-is-out/
* Carlo Agiuli wrote an introduction to the introduction:
http://www.carloangiuli.com/blog/homotopy-type-theory-univalent-foundations-of-mathematics/

If you're more of a visual person, watch a movie about the making of
the book (these are modern times): https://vimeo.com/68761218

With kind regards,

Andrej