I. Galvez-Carrillo, J. Kock, and A. Tonks. (2012)cite http://arxiv.org/abs/1207.6404arxiv:1207.6404Comment: v1: 48 pages, comments are welcome; v2: removed some material on graphs, expository improvements, 35 pages.
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)