Abstract:

Abstract: Around ten years ago, it was discovered that Martin-Lof's Intensional Type Theory - a logical system designed in the 1970's as a more constructive and computational alternative to ZFC-style foundations - admits quite unexpected interpretations in simplicial sets and other homotopy-theoretic settings. More than this: under this interpretation, the logic turned out to be remarkably powerful for expressing and reasoning with standard homotopy-theoretic properties and constructions, in very elementary ways. This connection has since proved extremely fruitful, and the resulting programme of work has become known as *Homotopy Type Theory* or *Univalent Foundations*.

In this talk, I will give a general introduction to type theory, and a survey of the recent homotopically-influenced developments - in particular, of the connections with $\infty$-toposes in the sense of Rezk/Lurie, for which it is hoped that type theory can provide an "internal language", in a certain precise sense.