|Time:|| 12:00 - 13:20
Wean Hall 7201
Department of Philosophy
Carnegie Mellon University
Homotopy type theory
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.
Here are some notes.