Thursday, February 22, 2018, from 4 to 5:30pm
East Hall, room 3088
Speaker: Chris Kapulkin (University of Western Ontario)
Title: Homotopy Type Theory and internal languages of higher categories
Homotopy Type Theory (or HoTT) is an approach to foundations of mathematics, building on the homotopy-theoretic interpretation of type theory. In addition to its foundational role, HoTT has been speculated to be the internal language of higher toposes in the sense of Joyal and Lurie.
This talk will be an introduction to HoTT, explaining its main ideas and presenting one way in which the connection between type theory and higher categories can be made precise.