Hofmann, Streicher: The groupoid interpretation of type theory

Martin Hofmann and Thomas Streicher, The groupoid interpretation of type theory, Twenty-five years of constructive type theory (Venice, 1995), Oxford Logic Guides, vol. 36, Oxford Univ. Press, New York, 1998, pp. 83–111.

(No abstract.) The first construction of a model in which identity types are non-trivial.

Full text at TS’s website. Mathscinet, Google Books.

@incollection {MR1686862,
    AUTHOR = {Hofmann, Martin and Streicher, Thomas},
     TITLE = {The groupoid interpretation of type theory},
 BOOKTITLE = {Twenty-five years of constructive type theory
              ({V}enice, 1995)},
    SERIES = {Oxford Logic Guides},
    VOLUME = {36},
     PAGES = {83--111},
 PUBLISHER = {Oxford Univ. Press},
   ADDRESS = {New York},
      YEAR = {1998},
   MRCLASS = {03B15 (68N15 68Q55)},
  MRNUMBER = {1686862},
}