Homotopical semantics of type theory

---

Mondays, 13:15–15:00 in EDIT 8103

One of the main ideas of homotopy type theory is that identity types in dependent type theory equip each type with a "path" structure. As a consequence, any model of type theory with identity types also has such a path structure on its objects, and can be seen as a "homotopy theory" (an (∞.1)-category). We'd like to also go the other way: given a homotopy theory, find a way to interpret type theory inside it so we can use type theory as a kind of domain-specific language for our homotopy theory. Indeed, we might dream of a correspondence between models of type theories with different connectives (products, functions) and homotopy theories with different structure. The idea of the course is to look at the current status of this dream: we know a lot more than we did 15 years ago, but there are still many unanswered questions. For some more specific sense of the kind of thing we'll be looking at, here's a foundational paper on the subject:

The homotopy theory of type theories
Chris Kapulkin and Peter LeFanu Lumsdaine
Advances in Mathematics 337 (2018) 1–38
doi:10.1016/j.aim.2018.08.003 · arXiv:1610.00037

I definitely don't expect you to be able to understand this paper at the start of the course; we'll be covering various parts of it as we go.

---

Schedule

---

26/01	|	1. Introduction, non-homotopical semantics of type theory
02/02	|	2. More non-homotopical semantics, higher categories
09/02	|	⋯
︙		⋱