Thorsten Altenkirch, Martin Hofmann’s contributions to type theory: Groupoids and univalence, Mathematical Structures in Computer Science 31 9 (2021) 953-957 [doi:10.1017/S0960129520000316]
On identity types in extensional/intensional dependent type theory (Martin-Löf dependent type theory):
whose chapter 2 on syntax and semantics of dependent type theory is also published as:
On the categorical semantics of dependent type theory with function types in locally cartesian closed categories (see at relation between category theory and type theory):
Martin Hofmann, On the interpretation of type theory in locally cartesian closed categories, in Computer Science Logic. CSL 1994, Lecture Notes in Computer Science 933 (1994) 427–441 [doi:10.1007/BFb0022273]
Pierre-Louis Curien, Richard Garner, Martin Hofmann, Revisiting the categorical interpretation of dependent type theory, Theoretical Computer Science 546 21 (2014) 99-119 [doi:10.1016/j.tcs.2014.03.003, pdf]
Introducing the homotopy type theory-interpretation of identity types (the “groupoid interpretation”)
and introducing what came to be known the univalence axiom (under the name “universe extensionality”):
Martin Hofmann, Thomas Streicher The groupoid interpretation of type theory, in: Giovanni Sambin et al. (eds.), Twenty-five years of constructive type theory, Proceedings of a congress, Venice, Italy, October 19-21, 1995, Oxf. Logic Guides. 36 Clarendon Press (1998) 83-111 [ISBN:9780198501275, ps.gz, pdf]
see also:
Ethan Lewis, Max Bohnet, The groupoid model of type theory, seminar notes (2017) [pdf, pdf]
Martin Hofmann, The groupoid interpretation of type theory, a personal retrospective, talk at HoTT at DMV2015 (2015) [slides]
On subtypes (with an early discussion of what came to be called lenses (in computer science), motivated by object-oriented programming):
Last revised on November 6, 2023 at 10:09:58. See the history of this page for a list of all contributions to it.