3
$\begingroup$

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?

$\endgroup$
4
  • $\begingroup$ This question seems better suited for proofassistants.stackexchange.com $\endgroup$ Sep 20 at 21:47
  • $\begingroup$ 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. $\endgroup$
    – Nift
    Sep 22 at 12:58
  • $\begingroup$ Perhaps I misread "Are there any formalizations ..." and you did not mean actual formalizations in a proof assistant? $\endgroup$ Sep 22 at 13:51
  • $\begingroup$ 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. $\endgroup$
    – Nift
    Sep 22 at 16:45

1 Answer 1

3
$\begingroup$

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!

$\endgroup$
2
  • $\begingroup$ #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). $\endgroup$
    – Max New
    Sep 21 at 11:20
  • $\begingroup$ 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. $\endgroup$ Sep 21 at 13:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.