The Coq mailing list

[Kenneth Adam Miller <kennethadammiller AT gmail.com>]

Awesome! Thanks for your contribution! People like you who give away sophisticated information for free make the world a better place.

On Fri, Jun 21, 2013 at 9:08 AM, Edward Z. Yang <ezyang AT mit.edu> wrote:

Excellent! Will you be releasing Coq editions of the chapter exercises?

Edward

Excerpts from Andrej Bauer's message of Fri Jun 21 12:10:53 +0200 2013:

> 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