Michael Shulman, Univalence for inverse diagrams and homotopy canonicity, Mathematical Structures in Computer Science, Volume 25, Issue 5 ( From type theory and homotopy theory to Univalent Foundations of Mathematics ) June 2015 (arXiv:1203.3253, doi:/10.1017/S0960129514000565)

André Joyal, What is categorical type theory, various talks in 2013, (pdf)