Hostname: page-component-745bb68f8f-b95js Total loading time: 0 Render date: 2025-02-11T06:24:48.395Z 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: streicher@mathematik.tu-darmstadt.de
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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

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