M. Hofmann and T. Streicher, The groupoid interpretation of type theory, Twenty-five years of constructive type theory, vol.36, pp.83-111, 1995.

, The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics, 2013.