Homotopy type theory and Joyal's conjecture

Thursday, February 6, 2014 - 12:00
427 Thackeray Hall
Speaker Information
Chris Kapulkin
University of Pittsburgh

Abstract or Additional Information

This is the first in a series of three talks on Joyal's Conjecture in Homotopy Type Theory. Roughly speaking, the conjecture asserts that the formal system of type theory can be seen as the internal logic of higher categories in a similar way that higher order intuitionistic logic is the internal language of (1-)toposes. In this talk, I will cover the necessary background on Homotopy Type Theory, especially in connection with higher category theory, giving a precise statement of Joyal's Conjecture. 

Research Area