# Product (Category Theory) is Unique

## Theorem

Let $\mathbf C$ be a metacategory.

Let $A$ and $B$ be objects of $\mathbf C$.

Let $A \times B$ and $A \times' B$ both be products of $A$ and $B$.

Then there is a unique isomorphism $u: A \times B \to A \times' B$.

That is, products are unique up to unique isomorphism.

## Proof

Denote the implicit projections of the two products by:

$\begin{xy}\[email protected][email protected]+4mu{ & A \times B \[email protected]/_/[ddl]_*{\textrm{pr}_1} \[email protected]/^/[ddr]^*{\textrm{pr}_2} \\ & A \times' B \ar[dl]^*{\textrm{pr}'_1} \ar[dr]_*{\textrm{pr}'_2} \\ A & & B }\end{xy}$

By the UMP of $A \times' B$, there is a unique $u: A \times B \to A \times' B$ fitting the dashed arrow in:

$\begin{xy}\[email protected][email protected]+4mu{ & A \times B \[email protected]/_/[ddl]_*{\textrm{pr}_1} \[email protected]/^/[ddr]^*{\textrm{pr}_2} \[email protected]{-->}[d] \\ & A \times' B \ar[dl]^*{\textrm{pr}'_1} \ar[dr]_*{\textrm{pr}'_2} \\ A & & B }\end{xy}$

By the UMP of $A \times B$, there is a further unique $v: A \times' B \to A \times B$ fitting the dashed arrow in:

$\begin{xy}\[email protected][email protected]+4mu{ & A \times B \[email protected]/_/[ddl]_*{\textrm{pr}_1} \[email protected]/^/[ddr]^*{\textrm{pr}_2} \ar[d]^*{u} \\ & A \times' B \ar[dl]^*{\textrm{pr}'_1} \ar[dr]_*{\textrm{pr}'_2} \[email protected]{-->}[d] \\ A & A \times B \ar[l]^*{\textrm{pr}_1} \ar[r]_*{\textrm{pr}_2} & B }\end{xy}$

We can now form the following diagram:

$\begin{xy}\[email protected][email protected][email protected]+4mu{ & A \times B \ar[dl]_*{\textrm{pr}_1} \ar[dr]^*{\textrm{pr}_2} \[email protected]{-->}[d] \\ A & A \times B \ar[l]^*{\textrm{pr}_1} \ar[r]_*{\textrm{pr}_2} & B }\end{xy}$

where we see both the identity morphism $\operatorname{id}_{A \times B}$ and $v \circ u$ fit the dashed arrow.

The UMP of $A \times B$ however states that there is a unique fitting morphism.

Hence $v \circ u = \operatorname{id}_{A \times B}$.

That $u \circ v = \operatorname{id}_{A \times' B}$ follows, mutatis mutandis, by interchanging $A \times B$ and $A \times' B$.

Hence there is a unique isomorphism $u: A \times B \to A \times' B$, as desired.

$\blacksquare$