Abstract:
Between the Logic and LogId seminars, I will give an introduction to and overview of the recent stream of work in type theory known variously as “homotopy type theory” and “univalent foundations”
The core idea is that Martin–Löf’s intensional dependent type theory admits models where types are interpreted as “spaces” in the sense of algebraic tomopoly/homotopy theory. Like any interesting interpretation, this can be used as a dictionary, translating concepts from homotopy theory into the language of type theory, and working with these within the theory.
In this talk, I will focus on the connections with homotopy theory: the mathematical models in homotopy-theoretic settings, and the use of type theory as a language for “synthetic homotopy theory”, including the idea and uses of higher inductive types.