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