Aarhus University Seal / Aarhus Universitets segl

QGM seminar by Ulrik Buchholtz (TU Darmstadt)

Title: Introduction to Homotopy Type Theory

2018.05.14 | Jane Jamshidi

Date Wed 16 May
Time 16:15 17:15
Location 1531-215 (Aud. D3)


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.