JournalsowrVol. 8 / No. 1DOI 10.4171/owr/2011/11

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
Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory cover

You need to subscribe to download the article.

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.