Can someone recommend introductory articles/papers on the connections between dependent type theory and locally cartesian closed category? Many Thanks!
$\begingroup$
$\endgroup$
1
-
3$\begingroup$ The original paper by Seely is quite readable: Locally cartesian closed categories and type theory. $\endgroup$– varkorFeb 16, 2021 at 20:20
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
The original interpretation of dependent type theory in lcccs by Seely suffers from coherence problems. There are a range of techniques with have been invented to solve them. In most cases the interpretation of a type $\Gamma \vdash A \textit{ type}$ is no longer an object in the slice $\mathbf S/\Gamma$ over the interpretation of $\Gamma$, instead the interpetation of $A$ will be a fibered functor $A:y(\Gamma)\to \partial_1$ where $\partial_1$ is the codomain fibration of the base. The fibered Yoneda lemma tells us that there is an equivalence $$Fib_\mathbf S(y\Gamma,\partial_1) = \mathbf S/\Gamma$$ The extra data which a fibered functor $A:y(\Gamma)\to \partial_1$ carries around is a choice of pullbacks of its display map in $\mathbf S/\Gamma$, and this is what is needed to solve the coherence problem. You asked for references, so here are some:
On the interpretation of type theory in locally cartesian closed categories by Martin Hoffman explains the coherence problem in Selly's semantic and explains how one can solve it.
More generally, the constructions in Hoffman's paper is just a way to associate a model of dependent type theory to a lcccs. You may want to read about such models in general. There are many different ones, but they are all essentially equivalent. E.g. there are categories with families, categories with attributes and split comprehension categories.
The later chapters of Jacobs Categorical Logic and Type Theory talk about comprehension and split comprehension categories. They do not discuss the canonical splitting of the self-indexing $\partial_1$ though.
Natural Models of Homotopy Type Theory by Awodey discusses the interpretation of $\Sigma,\Pi$ and extensional equality in a category in a really nice way.
Categories with Families Unityped, Simply Typed, and Dependently Typed by Castellan, Lairambault, Dybjer discusses in detail the 2-equivalence between the 2-category of lcccs and the 2-category of democatric categories with families which admit $\Pi,\Sigma,=,\mathbf 1$. I believe they also show that the syntax of Martin-Löf dependent type theory yields a 2-initial (in the non-strict sense) category with families. Together with the 2-equivalence to lcccs one can conclude that the category of contexts of MLTT with $\Pi,\Sigma,\mathbf 1,=$ is 2-intial in lccc.
The shorter article The biequivalence of lccc and MLTT by Clairambault, Dybjer is only about the relation between lcccs and MLTT, so it is exactly what you are looking for.
