\begin{definition}[Definition:Product (Category Theory)/Binary Product]
Let $\mathbf C$ be a metacategory.
Let $A$ and $B$ be objects of $\mathbf C$.
A '''(binary) product diagram''' for $A$ and $B$ comprises an object $P$ and morphisms $p_1: P \to A$, $p_2: P \to B$:
::$\begin{xy}\xymatrix@+1em@L+3px{
 A
&
 P
  \ar[l]_*+{p_1}
  \ar[r]^*+{p_2}
&
 B
}\end{xy}$
subjected to the following universal mapping property:
:For any object $X$ and morphisms $x_1, x_2$ like so:
::$\begin{xy}\xymatrix@+1em@L+3px{
 A
&
 X
  \ar[l]_*+{x_1}
  \ar[r]^*+{x_2}
&
 B
}\end{xy}$
:there is a unique morphism $u: X \to P$ such that:
::$\begin{xy}\xymatrix@+1em@L+3px{
&
 X
  \ar[ld]_*+{x_1}
  \ar@{-->}[d]^*+{u}
  \ar[rd]^*+{x_2}
\\
 A
&
 P
  \ar[l]^*+{p_1}
  \ar[r]_*+{p_2}
&
 B
}\end{xy}$
:is a commutative diagram, i.e., $x_1 = p_1 \circ u$ and $x_2 = p_2 \circ u$.
In this situation, $P$ is called a '''(binary) product of $A$ and $B$''' and may be denoted $A \times B$.
Generally, one writes $\left\langle{x_1, x_2}\right\rangle$ for the unique morphism $u$ determined by above diagram.
The morphisms $p_1$ and $p_2$ are often taken to be implicit.
They are called '''projections'''; if necessary, $p_1$ can be called the '''first projection''' and $p_2$ the '''second projection'''.
{{expand|the projection definition may merit its own, separate page}}
\end{definition}