Constructive Type Theory and Homotopy

Steve Awodey

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.

https://www.ias.edu/video/univalent/awodey