T. Program. (2013)cite http://arxiv.org/abs/1308.0729arxiv:1308.0729Comment: 465 pages. arXiv v1: first-edition-257-g5561b73, formatted for online reading. The most recent version, copies formatted for printing, and bound copies, are available at http://homotopytypetheory.org/book/.
M. Hofmann, and T. Streicher. Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, Oxford Univ. Press, New York, (1998)
D. Gepner, and J. Kock. (2012)cite http://arxiv.org/abs/1208.1749arxiv:1208.1749Comment: 26 pages. Comments are very welcome; v2: clarified some points in the introduction, minor expository changes, added one reference. No changes in theorems and proofs.
M. Bezem, T. Coquand, and S. Huber. 19th International Conference on Types for Proofs and Programs (TYPES 2013), volume 26 of Leibniz International Proceedings in Informatics (LIPIcs), page 107--128. Dagstuhl, Germany, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, (2014)