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.
INTRODUCTION TO THE UNIVALENT FOUNDATIONS OF MATHEMATICS
Constructive Type Theory and Homotopy
Fri, 12/03/2010 -
11:00 to 12:00