## Semantics of (homotopy) type theory ## (References, and some notes, for PLL’s tutorial 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. Another overview can be found at [[nlab:categorical model of dependent types]]. ### Contextual Categories John Cartmell, [Generalised algebraic theories and contextual categories](http://www.ams.org/mathscinet-getitem?mr=865990), 1986; Thomas Streicher, [Semantics of Type Theory](http://www.ams.org/mathscinet-getitem?mr=1134134), 1991. Very elementarily defined, and stratified by definition. ### Categories with Attributes, aka Type-categories John Cartmell, PhD thesis, [Generalised Algebraic Theories and Contextual Categories](https://dl.dropbox.com/u/2363336/CartmellThesis.pdf), 1978; Eugenio Moggi, [A category-theoretic account of program modules](http://www.ams.org/mathscinet-getitem?mr=1108806), 1989/1991; Andy Pitts, [Categorial Logic](http://www.ams.org/mathscinet-getitem?mr=1859470), 2000 (as type-categories). Fairly elementarily defined. Stratified 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. * Peter Dybjer, [Internal Type Theory](http://www.ams.org/mathscinet-getitem?mr=1474535), 1996; [http://www.cse.chalmers.se/~peterd/papers/InternalTT.pdf](http://www.cse.chalmers.se/~peterd/papers/InternalTT.pdf) * Martin Hofmann, [Syntax and Semantics of Dependent Types](http://www.ams.org/mathscinet-getitem?mr=1629519), 1997: [http://www.pps.univ-paris-diderot.fr/~mellies/mpri/mpri-ens/articles/hofmann-syntax-and-semantics-of-dependent-types.pdf](http://www.pps.univ-paris-diderot.fr/~mellies/mpri/mpri-ens/articles/hofmann-syntax-and-semantics-of-dependent-types.pdf) * Notes by Thierry Coquand on CwF are here: [what is a model of type theory](http://uf-ias-2012.wikispaces.com/file/view/cwf1.pdf/373011668/cwf1.pdf)? * Notes by Steve Awodey on CwF as a representable maps of presheaves: [notes on models of type theory](http://uf-ias-2012.wikispaces.com/file/view/notesTT.pdf/370624132/notesTT.pdf). * Pierre Clairambault and Peter Dybjer, [The biequivalence of locally cartesian closed categories and Martin-Löf type theory](http://uf-ias-2012.wikispaces.com/Semantics+of+type+theory#http://www.cse.chalmers.se/~peterd/papers/TLCA2011.pdf), 2011. ### Comprehension Categories * Bart Jacobs, [Comprehension categories and the semantics of type dependency](http://www.ams.org/mathscinet-getitem?mr=1201808), 1993. More abstractly formulated than the others above, and more general by default. Full split 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 e.g. substitution may not be functorial on the nose. #### Coherence for interpretation in comprehension categories * Pierre-Louis Curien, [Substitution up to isomorphism](http://uf-ias-2012.wikispaces.com/file/view/substitution.pdf/418826938/substitution.pdf), 1993. * Pierre-Louis Curien, Richard Garner and Martin Hofmann, [Revisiting the categorical interpretation of dependent type theory](http://uf-ias-2012.wikispaces.com/file/view/CGH-Glynn-anniv-2013.pdf/418828064/CGH-Glynn-anniv-2013.pdf), 2013. ### Joyal's Categorical Homotopy Type Theory Andr'e Joyal's approach based on the notion of a "tribe". Slides from a talk available here [[MIT.pdf:file]]. ### Natural Models Steve Awodey's functorial reformulation of category-with-families semantics, including a theorem providing [[natural model]]s in many homotopical categories. [Draft paper from 28 May 2014 here.](http://www.andrew.cmu.edu/user/awodey/preprints/natural.pdf) ### Introductions and surveys Bart Jacobs book; Martin Hofmann 1997 paper; PLL thesis. Sec 1.2; [nLab page](/nlab/show/categorical+model+of+dependent+types) [[!redirects Semantics]] [[!redirects semantics of type theory]]