The concept of cartesian product 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 . (In Set, would be the index set of the family, and the fiber of the bundle over an element of would be the set indexed by . Conversely, given a family of sets, can be constructed as its disjoint union.)
In these terms, the cartesian product of the family of sets is the set of (global) sections of the bundle. This set comes equipped with an evaluation map such that
equals the usual product projection; in other words, is a morphism in the over category . The universal property of is that, given any set and morphism in , there's a unique map that makes everything commute.
In other words, and define an adjunction from to in which taking the product with 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 to an arbitrary over category .
We also consider dependent sums, which are actually simpler.
For a category, the dependent product of the morphism indexed by the morphism is an object in the over category , where the operation is the right adjoint to the base change functor . For this to make sense, must exist; that is, all pullbacks along must exist. So a category with all dependent products is necessarily a category with all pullbacks.
In type theory, the operation of dependent product is typically taken as a primitive; see dependent product type. When employing the Curry–Howard correspondence, one sometimes (such as in Coq) writes as written , because dependent products correspond to universal quantification.
The left adjoint to the base-change functor, the dependent coproduct or dependent sum , is much simpler. It is simply given by composition with , so it always exists when it makes sense (that is when has all pullbacks). In the Curry–Howard correspondence, this corresponds to the particular quantification . See dependent sum type.
Note that the binary cartesian product is a special case of the direct sum: when is a constant family, i.e. a projection from a binary product, then its dependent sum is just the ordinary cartesian product . In this context, the dependent product can be identified with the exponential object . In other words, dependent sums generalize ordinary products, while dependent products generalize ordinary exponentials. (For this reason, one occasionally finds the dependent sum called the “dependent product”.) This is essentially a categorified version of the familiar fact that the product of two natural numbers can be identified with the sum of copies of .
Let be a cartesian closed category with all limits. Let be any object.
Then the dependent product functor
sends bundles to their object of sections
One computes for every
This statement and its proof remain valid in homotopy theory. More in detail, if is a simplicial model category, , and are cofibrant, and are fibrant and is a fibration, then as above is the homotopy-correct derived section space.
In terms of the internal logic of categories, when one considers propositions as types, one has that
dependent sum corresponds to existential quantification;
dependent product corresponds to universal quantification.
See there for more details.
Dependent products (and sums) exist in any topos:
For a topos and any morphism in , both the left adjoint as well as the right adjoint to exist.
Moreover, 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