Skip to main content
Get your brand new Wikispaces Classroom now
and do "back to school" in style.
Pages and Files
Categorical Semantics WG
Coq for UF
Coq Working Group
Formalized Homotopy Theory
Higher Inductive Types
Homotopy Type System
how to add a plugin
IAS program participants
Informal Type Theory
Math in HoTT
Modal type theory
Notation and terminology
Add "All Pages"
Semantics of type theory
(References, and some notes, for PLL’s
on the topic, Fri 28 Sep.)
There are various different categorical models for dependent type theory available in the literature. Most are equivalent, or almost so. Here we collect the various definitions, together with (hopefully definitive) references. If you have trouble tracking down any of these refs, email me [PLL]. All equivalences asserted are literal equivalences of 1-categories.
Generalised algebraic theories and contextual categories
, 1986; Thomas Streicher,
Semantics of Type Theory,
Very elementarily defined, and stratified by definition.
Categories with Attributes, aka Type-categories
John Cartmell, PhD thesis, 1978,
Generalised Algebraic Theories and Contextual Categories, 1978
; Eugenio Moggi,
A category-theoretic account of program modules
1989/1991; Andy Pitts,
Fairly elementarily defined.
CwA’s are equivalent to contextual categories.
Categories with Families
Classically equivalent to CwA’s, but formulated slightly differently to be better-suited to formalisation.
It can also be seen as a variable-free presentation of Martin-Lof's substitution calculus.
Internal Type Theory
Syntax and Semantics of Dependent Types
Notes by Thierry Coquand on CwF are here:
what is a model of type theory?
Notes by Steve Awodey on CwF as a representable maps of presheaves:
notes on models of type theory
Pierre Clairambault and Peter Dybjer,
The biequivalence of locally cartesian closed categories and Martin-Löf type theory,
Comprehension categories and the semantics of type dependency
More abstractly formulated than the others above, and more general by default.
comprehension categories are equivalent to CwA’s. The extra generality of comprehension cats is very useful for understanding the relationship with natural categorical models, where eg substitution may not be functorial on the nose.
Coherence for the interpretation of type theory in comprehension categories
Substitution up to isomorphism
Pierre-Louis Curien, Richard Garner and Martin Hofmann,
Revisiting the categorical interpretation of dependent type theory
Introductions and surveys
Bart Jacobs book; Martin Hofmann 1997 paper; PLL thesis. Sec 1.2;
help on how to format text
Turn off "Getting Started"