Indexed Cartesian Product

An indexed cartesian product in a Category $\mathcal{C}$ is an infinitary version of a Cartesian Product.

Explicitly, an $I$-indexed cartesian product of a family of objects $X_{i}$ is an object $\prod_{(i:I)}X_{i}$, along with projections maps $\pi_{i}:\prod_{(i:I)}X_{i}\to X_{i}$ that satisfy the following universal property:

• For any other object $P$ equipped with maps $p_{i}:P\to X_{i}$, there is a unique universal map $u:P\to\prod_{(i:I)}X_{i}$ where for every $i:I$, $\pi_{i}\circ u=p_{i}$.

Properties

• An indexed cartesian product is a Limit over a Discrete Category.
• An indexed cartesian product over the Booleans is a Cartesian Product.
• An indexed cartesian product over the Empty Type is a Terminal Object.
• An indexed cartesian product of a single object $X$ is a Power Object.

Global Defintion

A category has all $I$-indexed products whenever the functor $\Delta:\mathcal{C}\to\mathcal{C}^{I}$ that sends an object $X$ to the constant family $i\mapsto X$ has a Right Adjoint.