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?



Dependent sum/product and the base-change functor adjunctions
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](https://github.com/andrejbauer/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.


