5
$\begingroup$

I feel like I understand the construction of dependent product types relatively well, it makes sense to me how the introduction and elimination rules work together to create the concept of a function whose co-domain depends on the values of the function in the domain, but given the definitions and motivation on n-cat lab for the corresponding notion in category theory, I don't get the same intuition.

Given an element $x : I \rightarrow A$ in a category, and a categorical dependent product $f = \Pi_{x : A} F(x) $, it isn't even clear to me how one would obtain the element $f(x) : F(x)$, like one can using the elimination rule of the dependent product in type theory. More generally, I'd like to see a more explicit connection with the dependent product in type theory.

$\endgroup$
1
  • 1
    $\begingroup$ Do categorical semantics for the simply typed lambda calculus make sense to you? In particular, is it clear to you how the STLC rule $\frac{\Gamma \vdash f : A \to B \quad \Gamma \vdash x : A}{\Gamma \vdash f x : B}$ is interpreted? $\endgroup$ Commented Feb 7, 2016 at 19:36

1 Answer 1

7
$\begingroup$

Uff. It's hard to talk about this without introducing all of categorical type theory. The general notion is the notion of a comprehension category which I believe was introduced by Bart Jacobs. See his book or his thesis. However, when I did a search to get a reference for some definitions I found this recent set of notes, "Type Theory through Comprehension Categories" by Paolo Capriotti, which is pretty good.

We start with a category $\mathcal{C}$ whose objects we're going to think of as contexts which we'll think of as roughly lists of types. Given this, the type $\tau$ in context $\Gamma$ will be represented by an arrow $p_\tau : \Gamma,\tau\longrightarrow\Gamma$ called a display map which will be used to represent weakening. (Usually, only a subset of arrows will be designated as display maps.) We might notate a type-in-context as $\Gamma \vdash \tau$. So a type over $\Gamma$ is an object of the slice category $\mathcal{C}/\Gamma$. A term, $M$, of type $\tau$ is an arrow $M : \Gamma\longrightarrow\Gamma,\tau$ such that $p_\tau \circ M = id$. Typically this would be notated as $\Gamma \vdash M : \tau$. In other words, $M$ is an arrow from $id_\Gamma \to p_\tau$ in $\mathcal{C}/\Gamma$. An arbitrary arrow in $\mathcal{C}$, $\sigma : \Delta\longrightarrow\Gamma$ represents a substitution. Intuitively, it's a substitution for variables in $\Gamma$ in terms of variables in $\Delta$. These arrows give rise to functors $\sigma^* : \mathcal{C}/\Gamma\longrightarrow \mathcal{C}/\Delta$. To interpret $\sigma^*$ we require $\mathcal{C}$ to have pullbacks.

$$\require{AMScd} \begin{CD} \Delta,\tau[\sigma] @>>> \Gamma,\tau \\ @V\sigma^*(p_\tau)VV @VVp_\tau V \\ \Delta @>>\sigma> \Gamma \end{CD}$$

The action of $\sigma^*$ on arrows, i.e. terms, we might notate as $\Delta \vdash M[\sigma] : \tau[\sigma]$. The operation $(-)^*$ is itself pseudofunctorial meaning it preserves composition and identities only up to isomorphism. (This pseudofunctoriality, while a little to rigid to be completely natural categorically [it corresponds to a cloven fibration], is too loose type theoretically where, because we have syntax, we expect everything to hold "on the nose". Getting strict functoriality precipitates a lot of the complexity in this field.)

With that in place, the dependent product for a type $\tau$ is the right adjoint of $p_\tau^*$. $p_\tau^* \dashv \Pi_\tau : \mathcal{C}/\Gamma,\tau \to \mathcal{C}/\Gamma$. (Obviously we are going to want the adjoint to exist for all types and for them to fit together appropriately. The coherence conditions are called the Beck-Chevalley conditions.) We can write the action of $\Pi_\tau$ on a type as $$\frac{\Gamma,x:\tau\vdash B}{\Gamma\vdash\Pi x:\tau.B}$$ In particular we have the natural isomorphism $$\mathcal{C}/\Gamma,A(p_A^*(-),=) \cong \mathcal{C}/\Gamma(-, \Pi_A(=))$$ which if we instantiate to $id_\Gamma$ and $p_B$ gives a mapping on arrows (essentially terms) that in type theoretic notation would look like $$\frac{\Gamma,x:A\vdash M:B}{\Gamma\vdash\lambda x\!:\!A.M : \Pi x\!:\!A.B}$$ and post-composition by the counit gives a natural transformation of hom-functors $$\mathcal{C}/\Gamma,A(-,p_A^*(\Pi_A(=))) \to \mathcal{C}/\Gamma,A(-,=)$$ which, instantiating with $id_{\Gamma,A}$ and $p_B$, gives $$\frac{\Gamma,x:A\vdash M:\Pi y\!:\!A.B}{\Gamma,x:A\vdash Mx : B[y\mapsto x]}\quad x \text{ not free in } B$$

This rule represents a commutative triangle to which we can apply the substitution functor induced by the (underyling arrow of the) term $\Gamma \vdash N : A$ to get the more usual $$\frac{\Gamma\vdash N:A \quad \Gamma\vdash M:\Pi x\!:\!A.B}{\Gamma\vdash MN : B[x\mapsto N]}$$ (Actually this is slightly different from what I stated and more corresponds to doing $\sigma^*(\varepsilon_{p_B} \circ M[p_A^*])$ where $\sigma$ is the substitution induced by $N$.)

I've been fairly sloppy in this presentation, assuming certain properties hold strictly that may not. See the links above for explications of those details and how to deal with them.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .