All-around awesome logician colleagues and friends Steve Awodey and Jeremy Avigad have netted a $7.5m, 5-year grant to develop Homotopy Type Theory!

http://www.cmu.edu/news/stories/archives/2014/april/april28_awodeygrant.html

HoTT awarded a MURI