nLab Martin Hofmann

• webpage

Selected writings

On identity types in extensional/intensional dependent type theory (Martin-Löf dependent type theory):

• Martin Hofmann, Extensional concepts in intensional type theory, Ph.D. thesis, University of Edinburgh (1995), Distinguished Dissertations, Springer (1997) [ECS-LFCS-95-327, pdf, doi:10.1007/978-1-4471-0963-1]

whose chapter 2 on syntax and semantics of dependent type theory is also published as:

• Martin Hofmann, Syntax and semantics of dependent types, in Semantics and logics of computation, Publ. Newton Inst. 14, Cambridge Univ. Press (1997) 79-130 [doi:10.1017/CBO9780511526619.004]

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”):

• 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]

Related entries

• relation between category theory and type theory

• judgement

• homotopy type theory

category: people