Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory

  • Steve Awodey

    Carnegie-Mellon University, Pittsburgh, USA
  • Richard Garner

    Macquarie University, Sydney, Australia
  • Per Martin-Löf

    Stockholm University, Sweden
  • Vladimir Voevodsky

    Institute for Advanced Study, Princeton, USA

Abstract

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–638

DOI 10.4171/OWR/2011/11