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
    $\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$ – Derek Elkins left SE Feb 7 '16 at 19:36
6
$\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.

| cite | improve this answer | |
$\endgroup$

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.