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; in other words, $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. Let $X \in C$ be any object.
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 the above one obtains exponential objects/internal homs.
Let $\mathcal{C}$ have a terminal object $* \in \mathcal{C}$. Let $X \in \mathcal{C}$ be any object and let $X \colon X \to *$ be the terminal morphism.
The dependent product along $X$ of the base change along $X$ is the exponential object/internal hom $[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$.
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 | $\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}$ | |
term introduction | $\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 | $\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