<p>For  simple type theories, there's a very simple dictionary.</p>
<div class="s-table-container">
<table class="s-table">
<thead>
<tr>
<th><strong>Type Theory</strong></th>
<th><strong>Category Theory</strong></th>
</tr>
</thead>
<tbody>
<tr>
<td>Judgement</td>
<td>Category</td>
</tr>
<tr>
<td>Type</td>
<td>Object</td>
</tr>
<tr>
<td>Context</td>
<td>(Monoidal) Product</td>
</tr>
<tr>
<td>Term</td>
<td>Morphism</td>
</tr>
</tbody>
</table>
</div>
<p>However, interpreting dependent type theories is much more subtle, because the interpretation of a type is dependent on the <em>values</em> of the context: the type in context <span class="math-container">$b:2 \vdash \mathsf{if}\,b\,\mathsf{then}\, \Bbb{N} \,\mathsf{else}\,1$</span> is either the type of natural numbers or the unit type, depending on the value of <span class="math-container">$b$</span>.</p>
<p>The obvious thing to do when interpreting type theories in <span class="math-container">$\mathrm{Set}$</span> is just to interpret <span class="math-container">$\Gamma$</span> as the collection of closed substitutions inhabiting <span class="math-container">$\Gamma$</span>, and model <span class="math-container">$\Gamma \vdash A$</span> as a map <span class="math-container">$|\Gamma| \to \mathrm{Set}$</span>.</p>
<p>But that's not the only way! Here's another:</p>
<ol>
<li>Imagine that we have a closed type <span class="math-container">$\Sigma b:2.\,\mathsf{if}\,b\,\mathsf{then}\, \Bbb{N} \,\mathsf{else}\,1$</span>. This basically pairs a value for <span class="math-container">$b$</span> with a value of the dependent type.</li>
<li>Consider the first projection <span class="math-container">$\pi_1 : (\Sigma b:2.\,\mathsf{if}\,b\,\mathsf{then}\, \Bbb{N} \,\mathsf{else}\,1) \to 2$</span></li>
<li>If <span class="math-container">$\pi_1(b,v) = \mathsf{true}$</span>, then we know that <span class="math-container">$v$</span> must be a natural number.</li>
<li>If <span class="math-container">$\pi_1(b,v) = \mathsf{false}$</span>, then we know that <span class="math-container">$v$</span> is a unit value.</li>
<li>So the <em>inverse image</em> <span class="math-container">$\pi_1^{-1}(\mathsf{true}) = \Bbb{N}$</span>.</li>
<li>So the <em>inverse image</em> <span class="math-container">$\pi_1^{-1}(\mathsf{false}) = 1$</span>.</li>
</ol>
<p>So in general, we can think of a judgement <span class="math-container">$\Gamma \vdash A$</span> as being interpreted as the inverse images of <span class="math-container">$\pi_1 : (\Sigma \gamma:\Gamma. A) \to \Gamma$</span></p>
<p>This gives you the key idea for understanding models of dependent type theory. You need:</p>
<ol>
<li><p>A category <span class="math-container">$\Bbb{C}$</span> where <em>objects are contexts</em> and <em>morphisms are substitutions</em>. So a well-formed context <span class="math-container">$\Gamma\,\mathsf{ok}$</span> is an object <span class="math-container">$|\Gamma|$</span> in <span class="math-container">$\Bbb{C}$</span>.</p>
</li>
<li><p>A type-in-context <span class="math-container">$\Gamma \vdash A$</span> is a <span class="math-container">$\Bbb{C}$</span>-morphism in  <span class="math-container">$T : |A| \to |\Gamma|$</span>. The intuition is that you model the dependency of <span class="math-container">$A$</span> on <span class="math-container">$\Gamma$</span> via the inverse image operation. So if <span class="math-container">$\gamma \in |\Gamma|$</span>, we want <span class="math-container">$T^{-1}(\gamma) = A(\gamma)$</span>.</p>
</li>
<li><p>To model empty contexts, we use a unit object 1.</p>
</li>
<li><p>To model context extension, <span class="math-container">$|\Gamma, A|$</span>, what we do is we note that <span class="math-container">$id_{\Gamma} : |\Gamma| \to |\Gamma|$</span> and <span class="math-container">$T : |A| \to |\Gamma|$</span>, and then take the <em>pullback</em> of <span class="math-container">$id_{|\Gamma|}$</span> and <span class="math-container">$T$</span>. Set-theoretically, this is the &quot;fiber product&quot; -- it is the set of pairs <span class="math-container">$(\gamma, a)$</span> where <span class="math-container">$a \in T^{-1}(\gamma)$</span>.</p>
</li>
<li><p>A term-in-context <span class="math-container">$\Gamma \vdash e : A$</span> is a map <span class="math-container">$|e| : |\Gamma| \to |\Gamma,A|$</span> such that <span class="math-container">$|e|; p_1 = id_{|\Gamma|}$</span>. Here, <span class="math-container">$p_1$</span> is the first projection of the pullback <span class="math-container">$|\Gamma, A|$</span>. What this says is that the <span class="math-container">$|e|(\gamma) = (\gamma, a)$</span>, where <span class="math-container">$a \in T^{-1}(\gamma)$</span>.</p>
</li>
</ol>
<p>Finally, I've been a little low-level here. It's technically more convenient to use the &quot;slice category&quot; construction when working with maps <span class="math-container">$|A| \to |\Gamma|$</span>, because that packages up some of the coherence conditions (like the one in 5) in a nice way.</p>
<p>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 <span class="math-container">$T : |A| \to |\Gamma|$</span> with a substititution <span class="math-container">$\sigma : |\Delta| \to |\Gamma|$</span> and you'll learn why category theorists talk about substitution as pullback!</p>

CC BY-SA 4.0
2022-09-21T11:20:52.567Z
#4 is a bit odd. The object |A| is already the interpretation of |\Gamma , A|, and the pullback of a morphism along an identity is itself (up to isomorphism).
Max New
CC BY-SA 4.0
2022-09-21T13:54:43.957Z
If you have a function $f : A \to B$, then you know that $A \simeq \Sigma b:B. f^{-1}(b)$, but $A$ is not necessarily a set of pairs.  Similarly, $|A|$ is isomorphic to $|\Gamma, A|$, but doesn't necessarily contain pairs of environments and values. This doesn't matter semantically, but to see how the set-theoretic interpretation lurks within the categorical one, sometimes it is clarifying to shift one set to a different, isomorphic one. YMMV, of course.
Neel Krishnaswami
CC BY-SA 4.0
2022-09-21T10:00:49.053Z
2022-09-21T10:00:49.053Z
Neel Krishnaswami
<p>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?</p>

CC BY-SA 4.0
2022-09-20T21:47:48.870Z
This question seems better suited for https://proofassistants.stackexchange.com
Andrej Bauer
CC BY-SA 4.0
2022-09-22T12:58:20.693Z
I am willing to move it, but I feel like this is more of a foundations issue and less of a proof assistant implementation/usage one.
Ilk
CC BY-SA 4.0
2022-09-22T13:51:50.970Z
Perhaps I misread "Are there any formalizations ..." and you did not mean actual formalizations in a proof assistant?
Andrej Bauer
CC BY-SA 4.0
2022-09-22T16:45:20.373Z
I dont mind, rigorous paper ones are welcome too, just looking for a type theoretic point of view on categorical models, connecting type theoretic specification of smaller type theory to categorical models.
Ilk
<type-theory><ct.category-theory><model-theory>
Exposition of categorical models of type theory from type-theoretic perspective
Ilk
# Exposition of categorical models of type theory from type-theoretic perspective

(Asked by: username_0 on 2022-09-20)

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?

**Tags:** type-theory, ct.category-theory, model-theory

> **Comments:**
> **username_1**: This question seems better suited for https://proofassistants.stackexchange.com  
> **username_0**: I am willing to move it, but I feel like this is more of a foundations issue and less of a proof assistant implementation/usage one.  
> **username_1**: Perhaps I misread "Are there any formalizations ..." and you did not mean actual formalizations in a proof assistant?  
> **username_0**: I dont mind, rigorous paper ones are welcome too, just looking for a type theoretic point of view on categorical models, connecting type theoretic specification of smaller type theory to categorical models.  

---

## 1 answers

### Answer by username_2 on 2022-09-21. Score: 3 | Accepted answer

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!

> **Comments:**
> **username_3**: #4 is a bit odd. The object |A| is already the interpretation of |\Gamma , A|, and the pullback of a morphism along an identity is itself (up to isomorphism).  
> **username_2**: If you have a function $f : A \to B$, then you know that $A \simeq \Sigma b:B. f^{-1}(b)$, but $A$ is not necessarily a set of pairs.  Similarly, $|A|$ is isomorphic to $|\Gamma, A|$, but doesn't necessarily contain pairs of environments and values. This doesn't matter semantically, but to see how the set-theoretic interpretation lurks within the categorical one, sometimes it is clarifying to shift one set to a different, isomorphic one. YMMV, of course.  

---

