nLab Martin Hofmann

Selected writings

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

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

On subtypes (with an early discussion of what came to be called lenses (in computer science), motivated by object-oriented programming):

category: people

Last revised on November 6, 2023 at 10:09:58. See the history of this page for a list of all contributions to it.