Over the past few years it has become apparent that there is a surprising and deep connection between constructive logic and higherdimensional structures in algebraic topology and category theory, in the form of an interpretation of the dependent type theory of Per Martin-Löf into classical homotopy theory. The interpretation results in a bridge between the worlds of constructive and classical mathematics which promises to shed new light on both. This mini-workshop brought together researchers in logic, topology, and cognate fields in order to explore both theoretical and practical ramifications of this discovery.
Cite this article
Steve Awodey, Richard Garner, Per Martin-Löf, Vladimir Voevodsky, Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory. Oberwolfach Rep. 8 (2011), no. 1, pp. 609–638DOI 10.4171/OWR/2011/11