The Mathematical and Computational Sciences at Western are represented by four separate departments: Applied Mathematics, Computer Science, Mathematics, and Statistical & Actuarial Sciences. The Department of Mathematics has established research groups in several areas of contemporary mathematics including algebra, analysis and analytic geometry, homotopy theory, and noncommutative geometry.
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.