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},
}

One Response to Hofmann, Streicher: The groupoid interpretation of type theory

  1. Pingback: #HoTT The Book 2.1 Types are higher groupoids | Autrement qu'être Mathesis uni∜ersalis Problema Universale Heidegger/Husserl être/conscience : plan vital-ontologique vs plan spirituel d'immanence CLAVIS UNIVERSALIS HENOSOPHIA PANSOPHIA εν

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s