Oberwolfach Reports

Full-Text PDF (300 KB) | Introduction as PDF | Metadata | Table of Contents | OWR summary
Volume 8, Issue 1, 2011, pp. 609–638
DOI: 10.4171/OWR/2011/11

Published online: 2011-09-04

Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory

Steve Awodey[1], Richard Garner[2], Per Martin-Löf[3] and Vladimir Voevodsky[4]

(1) Carnegie-Mellon University, Pittsburgh, USA
(2) Macquarie University, Sydney, Australia
(3) Stockholm University, Sweden
(4) Institute for Advanced Study, Princeton, USA

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.

No keywords available for this article.

Awodey Steve, Garner Richard, Martin-Löf Per, Voevodsky Vladimir: Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory. Oberwolfach Rep. 8 (2011), 609-638. doi: 10.4171/OWR/2011/11