nLab Thomas Streicher

Selected writings

Selected writings

On categorical semantics of (dependent) type theory (and proving an initiality conjecture in Ch. 4), see at categorical model of dependent types:

On intensional type theory:

  • Thomas Streicher, Investigations into Intensional Type Theory, Habilitation Thesis, Darmstadt (1993) [pdf, pdf]

Introducing the homotopy type theory-interpretation of identity types (the “groupoid model”)

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. Oxford: Clarendon Press. Oxf. Logic Guides. 36 (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]

On category theory and categorical logic:

On denotational semantics and domain theory for functional programming languages:

On first-order set theory and categorical logic:

On fibered categories following Jean Bénabou:

A 2-comonad characterizing Grothendieck fibrations:

category: people

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