Homotopy Type Theory
Categorical Homotopy Type Theory

Joyal's Categorical HoTT, PDF of slides from a talk given by André Joyal at the MIT Topology Seminar, March 17, 2014.