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. and introducing what came to be known the univalence axiom (under the name “universe extensionality”):
Last revised on January 23, 2023 at 09:46:11. See the history of this page for a list of all contributions to it.