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]
On subtypes (with an early discussion of what came to be called lenses (in computer science), motivated by object-oriented programming):
Introducing the homotopy type theory-interpretation of identity types. and introducing what came to be known the univalence axiom (under the name “universe extensionality”):
Last revised on August 14, 2023 at 12:00:11. See the history of this page for a list of all contributions to it.