Internal Language of Higher Categories
Karol Szumilo – 22 November 2017, 29 November 2017
The theory of (infinity, 1)-categories can be seen as an abstract framework for homotopy theory which emerged from classical category theory and algebraic topology. Homotopy Type Theory is a formal language originating from logic which can also be used to argue about homotopy theory. It is believed that HoTT is an "internal language" of (infinity, 1)-categories. Roughly speaking, this means that HoTT and higher category theory prove the same theorems. Even making this statement precise is challenging and leads to a range of conjectures of varying scope and depth. In this talk, I will discuss a proof of the simplest of these conjectures obtained recently in joint work with Chris Kapulkin.
Back