Homotopical Interpretations of Type Theory

Karol Szumilo, University of Leeds. Part of the proofs, constructions and computations seminar series.

Martin-Löf Type Theory (MLTT) can be used as an approach to "synthetic homotopy theory", i.e., it provides a formal language in which one can formulate and prove theorems of topology in a purely homotopy invariant manner. This is sometimes described informally by saying that MLTT is the "internal language" of certain (infinity, 1)-categories, but it is difficult to make this statement precise. In this talk, I will give an overview of homotopical interpretations of MLTT culminating in a recent result, joint with Chris Kapulkin, that proves a weak version of the statement above, in analogy to a classical theorem of Lambek and Scott asserting that lambda-calculus is the internal language of cartesian closed categories.