|INTRODUCTION TO THE UNIVALENT FOUNDATIONS OF MATHEMATICS|
|Topic:||Constructive Type Theory and Homotopy|
|Affiliation:||Carnegie Mellon University|
|Date:||Friday, December 3|
|Time/Room:||11:00am - 12:00pm/S-101|
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.