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 http://homotopytypetheory.org/2014/04/29/hott-awarded-a-muri/