Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-26T19:41:51.362Z Has data issue: false hasContentIssue false
  • English
  • Français

The genesis of the groupoid model

Published online by Cambridge University Press:  29 December 2020

Thomas Streicher Open the ORCID record for Thomas Streicher [Opens in a new window]
Thomas Streicher*
Affiliation:
Fachbereich Mathematik, Technische Universität Darmstadt, Darmstadt, Germany
*
Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

I recall how Martin Hofmann and I found the groupoid model of type theory in the early 1990s.

Keywords

Type theorycategorical semanticshomotopy
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 31 , Special Issue 9: In Homage to Martin Hofmann , October 2021 , pp. 1003 - 1005
Check for updates
Copyright
© The Author(s), 2020. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Hofmann, M. and Streicher, T. (1994). The groupoid model refutes uniqueness of identity proofs. In: Proceedings of LiCS94, 208–212.10.1109/LICS.1994.316071CrossRefGoogle Scholar
Hofmann, M. and Streicher, T. (1996). The groupoid interpretation of type theory. In: Sambin, G. (ed.) Twenty-Five Years of Constructive Type Theory, OUP.Google Scholar
Seely, R. A. G. (1984). Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society 95(1) 33–48.10.1017/S0305004100061284CrossRefGoogle Scholar
Streicher, T. (1989). Semantics of Type Theory. Thesis University of Passau.Google Scholar
Streicher, T. (1994). Investigations into Intensional Type Theory. Habilitation Thesis, Ludwig Maximilians Universität, Munich.Google Scholar