Exposition of categorical models of type theory from type-theoretic perspective

Question

Are there any formalizations or expositions of categorical models from type theoretic point-of-view? What I have in mind to get a better grasp of categorical models of dependent types, treating categories as a type in some type theoretic universe and showcasing how to pass from inference system (as a let's say indexed type) for a universe-free type theory into a category and then back to properties of the inference system such as consistency (as an external non-inhabitance of an empty type), perhaphs showcasing what goes wrong for an inconsistent inference system. Are there currently any formalizations of this form?

Answer 1

For simple type theories, there's a very simple dictionary.

Type Theory	Category Theory
Judgement	Category
Type	Object
Context	(Monoidal) Product
Term	Morphism

However, interpreting dependent type theories is much more subtle, because the interpretation of a type is dependent on the values of the context: the type in context $b:2 \vdash \mathsf{if}\,b\,\mathsf{then}\, \Bbb{N} \,\mathsf{else}\,1$ is either the type of natural numbers or the unit type, depending on the value of $b$.

The obvious thing to do when interpreting type theories in $\mathrm{Set}$ is just to interpret $\Gamma$ as the collection of closed substitutions inhabiting $\Gamma$, and model $\Gamma \vdash A$ as a map $|\Gamma| \to \mathrm{Set}$.

But that's not the only way! Here's another:

1. Imagine that we have a closed type $\Sigma b:2.\,\mathsf{if}\,b\,\mathsf{then}\, \Bbb{N} \,\mathsf{else}\,1$. This basically pairs a value for $b$ with a value of the dependent type.
2. Consider the first projection $\pi_1 : (\Sigma b:2.\,\mathsf{if}\,b\,\mathsf{then}\, \Bbb{N} \,\mathsf{else}\,1) \to 2$
3. If $\pi_1(b,v) = \mathsf{true}$, then we know that $v$ must be a natural number.
4. If $\pi_1(b,v) = \mathsf{false}$, then we know that $v$ is a unit value.
5. So the inverse image $\pi_1^{-1}(\mathsf{true}) = \Bbb{N}$.
6. So the inverse image $\pi_1^{-1}(\mathsf{false}) = 1$.

So in general, we can think of a judgement $\Gamma \vdash A$ as being interpreted as the inverse images of $\pi_1 : (\Sigma \gamma:\Gamma. A) \to \Gamma$

This gives you the key idea for understanding models of dependent type theory. You need:

1. A category $\Bbb{C}$ where objects are contexts and morphisms are substitutions. So a well-formed context $\Gamma\,\mathsf{ok}$ is an object $|\Gamma|$ in $\Bbb{C}$.

2. A type-in-context $\Gamma \vdash A$ is a $\Bbb{C}$-morphism in $T : |A| \to |\Gamma|$. The intuition is that you model the dependency of $A$ on $\Gamma$ via the inverse image operation. So if $\gamma \in |\Gamma|$, we want $T^{-1}(\gamma) = A(\gamma)$.

3. To model empty contexts, we use a unit object 1.

4. To model context extension, $|\Gamma, A|$, what we do is we note that $id_{\Gamma} : |\Gamma| \to |\Gamma|$ and $T : |A| \to |\Gamma|$, and then take the pullback of $id_{|\Gamma|}$ and $T$. Set-theoretically, this is the "fiber product" -- it is the set of pairs $(\gamma, a)$ where $a \in T^{-1}(\gamma)$.

5. A term-in-context $\Gamma \vdash e : A$ is a map $|e| : |\Gamma| \to |\Gamma,A|$ such that $|e|; p_1 = id_{|\Gamma|}$. Here, $p_1$ is the first projection of the pullback $|\Gamma, A|$. What this says is that the $|e|(\gamma) = (\gamma, a)$, where $a \in T^{-1}(\gamma)$.

Finally, I've been a little low-level here. It's technically more convenient to use the "slice category" construction when working with maps $|A| \to |\Gamma|$, because that packages up some of the coherence conditions (like the one in 5) in a nice way.

To a computer scientist, this feels like a very inside-out way of thinking about indexed objects, but (a) people who know tell us it works better in the long run, and (b) it's kind of fun. Try to see how to compose a type in context $T : |A| \to |\Gamma|$ with a substititution $\sigma : |\Delta| \to |\Gamma|$ and you'll learn why category theorists talk about substitution as pullback!