The dependent product is a universal construction in category theory. It generalizes the internal hom, and hence indexed products, to the situation where the codomain may depend on the domain, hence it forms sections of a bundle.
The dual concept is that of dependent sum.
The concept of cartesian product of sets makes sense for any family of sets, while the category-theoretic product makes sense for any family of objects. In each case, however, the family is indexed by a set; how can we get a purely category-theoretic product indexed by an object?
First we need to describe a family of objects indexed by an object; it's common to interpret this as a bundle, that is an arbitrary morphism $g: B \to A$. (In Set, $A$ would be the index set of the family, and the fiber of the bundle over an element $x$ of $A$ would be the set indexed by $x$. Conversely, given a family of sets, $B$ can be constructed as its disjoint union.)
In these terms, the cartesian product of the family of sets is the set $S$ of (global) sections of the bundle. This set comes equipped with an evaluation map $ev: S \times A \to B$ such that
equals the usual product projection from $S \times A$ to $A$; So $ev$ is a morphism in the over category $Set/A$. The universal property of $S$ is that, given any set $T$ and morphism $T \times A \to B$ in $Set/A$, there's a unique map $T \to S$ that makes everything commute.
In other words, $S$ and $ev$ define an adjunction from $Set$ to $Set/A$ in which taking the product with $A$ is the left adjoint and applying this universal property is the right adjoint. This is the basis for the definition below, but we add one further level of generality: we move everything from $Set$ to an arbitrary over category $\mathcal{C}/I$.
Let $\mathcal{C}$ be a category, and $g\colon B \to A$ a morphism in $\mathcal{C}$, such that pullbacks along this morphism exist. These then constitute the base change functor between the corresponding slice categories
The dependent product along $g$ is, if it exists, the right adjoint functor $\prod_g \colon : \mathcal{C}_{/B} \to \mathcal{C}_{/A}$ to the base change along $g$
So a category with all dependent products is necessarily a category with all pullbacks.
Let $\mathcal{C}$ be a cartesian closed category with all limits and note that $\mathcal{C}/*\cong\mathcal{C}$. Let $X \in C$ be any object and identify it with the terminal morphism $X\to *$. Then the dependent product functor
sends bundles $P \to X$ to their object of sections.
One computes for every $A \in \mathcal{C}$
This statement and its proof remain valid in homotopy theory. More in detail, if $\mathcal{C}$ is a simplicial model category, $X$, $A$ and $X \times A$ are cofibrant, $P$ and $X$ are fibrant and $P \to X$ is a fibration, then $\Gamma_X(A)$ as above is the homotopy-correct derived section space.
As a special case of prop. 1 one obtains exponential objects/internal homs.
Let $\mathcal{C}$ have a terminal object $* \in \mathcal{C}$. Let $A$ and $X$ in $\mathcal{C}$ be objects and let $A \colon A \to *$ and $X \colon X \to *$ be the terminal morphisms.
The dependent product along $X$ of the arrow obtained by base change of $A$ along $X$ is the exponential object $[X,A]$:
This is essentially a categorified version of the familiar fact that the product $n\cdot m$ of two natural numbers can be identified with the sum $\overset{n}{\overbrace{m+\dots +m}}$ of $n$ copies of $m$.
Consider the chain of equivalences from $[X,A]$ to $\prod_{X} X^* A$ in Set: Firstly, the exponential object $[X,A]$ is characterized in $[Y,[X,A]]$ as right adjoint to $[Y\times X,A]$. Secondly, the elements $\theta$ of $[Y\times X,A]$ are in turn in bijection with those functions $(y,x)\mapsto (\theta(y,x),x)$ from $[Y\times X,A\times X]$, that leave the second component fixed. The condition just stated is the definition of arrows in the overcategory ${Set}/X$, between the right projections out of $Y\times X$ resp. $A\times X$. If we identify objects $Z\in{Set}$ with their terminal morphisms $Z:Z\to *$ in ${Set}/*$, those two right projections are the pullbacks $X^* Y$ and $X^* A$, respectively. Thirdly, thus, the subset of $[Y\times X,A\times X]$ we are interested in corresponds to $[X^* Y,X^* A]$ in ${Set}/X$. Finally, the right adjoint to $X^*$ is a functor $\prod_{X}$ from ${Set}/X$ to ${Set}/*$, such that $[X^* Y,X^* A]\simeq [Y, \prod_{X} X^* A]$. Hence $\prod_{X} X^* A$ must correspond to $[X,A]$.
The dependent product is the categorical semantics of what in type theory is the formation of dependent product types. Under propositions as types this corresponds to universal quantification.
type theory | category theory | |
---|---|---|
syntax | semantics | |
natural deduction | universal construction | |
dependent product type | dependent product | |
type formation | $\displaystyle\frac{\vdash\: X \colon Type \;\;\;\;\; x \colon X \;\vdash\; A(x)\colon Type}{\vdash \; \left(\prod_{x \colon X} A\left(x\right)\right) \colon Type}$ | $\left( \array{ A^{\phantom{p_1}} \\ \downarrow^{p_1} \\ X_{\phantom{p_1}}} \in \mathcal{C}\right) \Rightarrow \left( \prod_{x\colon X} A\left(x\right) \in \mathcal{C}\right)$ |
term introduction | $\displaystyle\frac{x \colon X \;\vdash\; a\left(x\right) \colon A\left(x\right)}{\vdash (x \mapsto a\left(x\right)) \colon \prod_{x' \colon X} A\left(x'\right) }$ | |
term elimination | $\displaystyle\frac{\vdash\; f \colon \left(\prod_{x \colon X} A\left(x\right)\right)\;\;\;\; \vdash \; x \colon X}{x \colon X\;\vdash\; f(x) \colon A(x)}$ | |
computation rule | $(y \mapsto a(y))(x) = a(x)$ |
Dependent products (and sums) exist in any topos:
For $C$ a topos and $f : A \to I$ any morphism in $C$, both the left adjoint $\sum_f : C/A \to C/I$ as well as the right adjoint $\prod_f: C/A \to C/I$ to $f^*: C/I \to C/A$ exist.
Moreover, $f^*$ preserves the subobject classifier and internal homs.
This is (MacLaneMoerdijk, theorem 2 in section IV, 7).
The dependent product plays a role in the definition of universe in a topos.
dependent sum, dependent product
Standard textbook accounts include section A1.5.3 of
and section IV of