Homotopical Interpretations of Type Theory
- Date: Wednesday 5 December 2018, 14:00 – 15:00
- Location: Mathematics Level 8, MALL 1, School of Mathematics
- Type: Proofs, Constructions and Computations, Seminars, Pure Mathematics
- Cost: Free
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.