In a category, a product (also called a cartesian product) of two objects $X$ and $Y$ is an object $X\times Y$ equipped with morphisms $p:X\times Y \to X$ and $q:X\times Y \to Y$, called projections, such that for any object $Z$ equipped with maps $f:Z\to X$ and $g:Z\to Y$ there exists a unique $h:Z\to X\times Y$ (called the pairing of $f$ and $g$) such that $p \circ h=f$ and $q \circ h=g$.
Such a categorical product is equivalently a limit over a diagram of the shape of the category $\{a,b\}$ with two objects and no non-trivial morphisms.
More generally, for $S \in$ Set $\hookrightarrow$ Cat any discrete category, an $S$-indexed limit is a product of $|S|$ factors. If $S$ is a finite set we speak of a finite product. Notice that this includes the case of the empty set, the product over which is, if it exists, the terminal object of the category in question.
When they exist, products are unique up to unique canonical isomorphism, so we often say “the product.”
One can define in a similar way a product of any family of objects. A product of the empty family is a terminal object.
A product is a special case of a limit in which the domain category is discrete.
A product in $C$ is the same as a coproduct in its opposite category $C^{op}$.
Under the relation between category theory and type theory products in a category correspond to product types in type theory.
type theory | category theory | |
---|---|---|
syntax | semantics | |
natural deduction | universal construction | |
product type | product | |
type formation | $\frac{\vdash \;A \colon Type \;\;\;\;\; \vdash \;B \colon Type}{\vdash A \times B \colon Type}$ | $A,B \in \mathcal{C} \Rightarrow A \times B \in \mathcal{C}$ |
term introduction | $\frac{\vdash\; a \colon A\;\;\;\;\; \vdash\; b \colon B}{ \vdash \; (a,b) \colon A \times B}$ | $\array{ && Q\\ & {}^{\mathllap{a}}\swarrow &\downarrow_{\mathrlap{(a,b)}}& \searrow^{\mathrlap{b}}\\ A &&A \times B&& B }$ |
term elimination | $\frac{\vdash\; t \colon A \times B}{\vdash\; p_1(t) \colon A} \;\;\;\;\;\frac{\vdash\; t \colon A \times B}{\vdash\; p_2(t) \colon B}$ | $\array{ && Q\\ &&\downarrow^{t} && \\ A &\stackrel{p_1}{\leftarrow}& A \times B &\stackrel{p_2}{\to}& B}$ |
computation rule | $p_1(a,b) = a\;\;\; p_2(a,b) = b$ | $\array{ && Q \\ & {}^{\mathllap{a}}\swarrow &\downarrow_{(a,b)}& \searrow^{\mathrlap{b}} \\ A &\stackrel{p_1}{\leftarrow}& A \times B& \stackrel{p_2}{\to} & B}$ |
This interactive demonstration in FinSet lets you type two sets and see a product, showing the unique map to it from a randomly chosen $Z$ equipped with $f$ and $g$. It also generates a second product, showing the unique canonical isomorphism between this and the first product.