Abstract: Type Theory was invented by the Swedish logician Per Martin-Loef in the early 1970's; its aim was to formalise "strictly constructive mathematics". Quite apart from this motivation, Type Theory is the underlying framework of various computer languages, in particular "proof assistants" such as Coq. It has remained a challenge, however, to give meaning to Type Theory in mathematical terms. In recent years, an interesting connection between Type Theory and Homotopy Theory has emerged, thanks to Awodey, Moerdijk, van den Berg, and others. This development has received new impetus from the interest that Vladimir Voevodsky (Fields Medal, 2002) takes in this area. Voevodsky aims to develop a new treatment of Foundations of Mathematics, based on a homotopy-type interpretation of Type Theory. The talk will explain the basic notions involved, and try to sketch some of the developments.
