The linked course pages contains a good synopsis, but Robert Harper's own blog post "What’s the big deal with HoTT?" [0] gives a wider view about its motivation

The linked course pages contains a good synopsis, but Robert Harper's own blog post "What’s the big deal with HoTT?" [0] gives a wider view about its motivation and history. Another two pages with worthwhile information on the HoTT book are [1] and [2]. [0] http://existentialtype.wordpress.com/2013/06/22/whats-the-big-deal-with-hott/ http://existentialtype.wordpress.com/2013/06/22/whats-the-bi... [1] http://golem.ph.utexas.edu/category/2013/06/the_hott_book.html http://golem.ph.utexas.edu/category/2013/06/the_hott_book.ht... [2] http://math.andrej.com/2013/06/20/the-hott-book/ http://math.andrej.com/2013/06/20/the-hott-book/