Constructive Type Theory and Homotopy

Download Embed
Steve Awodey
Institute for Advanced Study
December 3, 2010

In recent research it has become clear that there are fascinating connections between constructive mathematics, especially as formulated in the type theory of Martin-Löf, and homotopy theory, especially in the modern treatment in terms of Quillen model categories and higher-dimensional categories. This talk will survey some of these developments.