Thomas Streicher (1958–2025) On categorical semantics of (dependent) type theory (and proving an initiality conjecture in Ch. 4), see at categorical model of dependent types: 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 profunctors (distributors): 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: