Homotopy type theory and Joyal's conjecture

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.