Constructive Type Theory and Homotopy

INTRODUCTION TO THE UNIVALENT FOUNDATIONS OF MATHEMATICS
Topic:Constructive Type Theory and Homotopy
Speaker:Steve Awodey
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.