Chris Kapulkin: Homotopy Type Theory and internal languages of higher categories

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

Abstract:

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.

Leave a Reply

Your email address will not be published. Required fields are marked *

Time limit is exhausted. Please reload CAPTCHA.