Title: Introduction to Homotopy Type Theory
2018.05.14 |
| Date | Wed 16 May |
| Time | 16:15 — 17:15 |
| Location | 1531-215 (Aud. D3) |
Abstract:
Homotopy type theory is a subject in the intersection of type theory (a discpline concerning logic and the foundations of programming languages) and homotopy theory. I will give an introduction that emphasizes the homotopy theoretic aspects.
A dependent type theory augmented by Voevodsky's Univalence Axiom and new type formers called Higher Inductive Types, allow us to reason synthetically about the usual homotopy theory of spaces and also about
the objects of more exotic homotopy theories, as captured by infinity-toposes. Examples include homotopical refinements of Synthetic Differential Geometry a la Kock and Lawvere, as well as a synthetic theory of Quantum Field Theories being developed by Schreiber.
The talk will not require any background knowledge of type theory.
