Dependent sum/product and the base-change functor adjunctions

Question

In type theory, the dependent sum $\sum_{x : A} T(x)$ and the dependent product $\prod_{x:A} T(x)$ are defined by their introduction/elimination rules.

In category theory, we use a base-change functor. Given a morphism $f \colon b \to a$, we define the functor $f^* \colon C/a \to C/b$ between slice categories using a pullback. The dependent sum $\sum_f$ is then defined as the left adjoint, and the dependent product $\prod_f$ as the right adjoint to $f^*$.

My question is, what's the interpretation of $f$ ? It doesn't show in the type-theoretical definitions. It looks like one can get the type-theoretical definitions by picking $a$ to be the terminal object, with $f \colon b \to 1$ the unique terminal morphism $!$. Is there more to it?

Answer 1

The morphism $f$ is invisible in type theory because it corresponds to weakening, which in type theory appears as context extension, rather than an explicitly applied substitution.

Type-theoretic explanation

More precisely, given a context $\Gamma$ and a type family $\Gamma \vdash A \; \mathsf{type}$ there is a substitution $\iota : (\Gamma, x {:} A) \to \Gamma$ which takes each variable $y \in \Gamma$ to itself (but is not identity, it's shifting in terms of de Bruijn indices). This is your $f$. It induces a weakening operation $\iota^{*} : \mathsf{Type}(\Gamma) \to \mathsf{Type}(\Gamma, x{:}A)$ that takes a type family over $\Gamma$ to a type family over $\Gamma, x {:} A$. The dependent product and sum go in the opposite direction $$\Pi, \Sigma : \mathsf{Type}(\Gamma, x{:}A) \to \mathsf{Type}(\Gamma)$$ and their rules state precisely that there are adjunctions $\Sigma \vdash \iota^{*} \vdash \Pi$.

Set-theoretic explanation

Let us also explain what $\iota$ corresponds to set-theoretically. There are two equivalent ways of giving a set-theoretic interpretation, namely families and display maps. You indicated in your question that you prefer the latter, so let us use that. (The families are more natural, please consult Section 5.1 of my notes on realizability for details.)

A context is a set. The empty context is the singleton set.

A type family $\Gamma \vdash A \; \mathsf{type}$ is an element of the slice $\mathsf{Set}/\Gamma$, which we write as $p_A : \overline{A} \to \Gamma$.

A term of type $A$ in context $\Gamma$ is a section $t : \Gamma \to \overline{A}$ of $p_A$, i.e., it has to satisfy $p_A \circ t = \mathsf{id}$. In particular, this means that from $t(\gamma) \in \overline{A}$ we can reconstruct $\gamma = p_A(t(\gamma))$, which means that $t(\gamma)$ should not be thought of as "one element of $A$", but rather as "one element of $A$ together with an environment $\gamma$".

Given a type family $p_A : \overline{A} \to \Gamma$, the context extension $\Gamma, x {:} A$ is the set $\overline{A}$.

A substitution is a map $\sigma : \Gamma \to \Delta$. Specifically, the above substitution $\iota : (\Gamma, x {:} A) \to \Gamma$ is just the map $p_A : \overline{A} \to \Gamma$.

The action of $\sigma : \Gamma \to \Delta$ is pullback $$\sigma^* : \mathsf{Set}/\Delta \to \mathsf{Set}/\Gamma.$$ When we plug in $p_A$ we get the pullback $$p_A* : \mathsf{Set}/\Gamma \to \mathsf{Set}/\overline{A}.$$ It has left and right adjoints $\Sigma_A \dashv p_A^* \dashv \Pi_A$. I can spell them out if you wish.

Answer 2

Categorically, the right adjoint $\Pi_f$ exists when $f$ is exponentiable. In the categorical semantics of type theory, exponentiable maps correspond to the display maps. There are several ways one can think of display maps, but a simple way is to view a display map $f \colon B \to A$ as representing a type $B$ that depends on $A$. This means that whenever we have a context containing a variable of type $B$, we can form a term of type $A$. Type theoretically, we might write this as $a : A, b : B(a) \vdash a \colon A$ (or possibly leaving $a : A$ in the context implicit).

The base change functor $f^*$ therefore sends a morphism $t \colon \Gamma \to A$, understood as a term $\Gamma \vdash t : A$, to the projection morphism $f^* t \colon \Gamma \times_A B \to B$ from the pullback, which is understood to represent the term $\Gamma, b : B(t) \vdash b : B(t)$. (This is the mantra "pullback is substitution", or more specifically, "pullback is term-in-type substitution".)

If $B$ does not depend on a type $A$, then the display map is the unique morphism $! \colon B \to 1$, as in your example. So your interpretation is correct when there is no type dependency, but you need to be more careful when dealing with dependent types.