Uniqueness of categorical products

Question

I'm currently studying category theory out of Awodey's excellent online book, but I'm having trouble seeing that the mapping between two product objects is necessarily an iso.

If $P,p_0:P\rightarrow A,p_1:P\rightarrow B$ and $X,x_0:X\rightarrow A,x_1:X\rightarrow B$ are product diagrams for $A$ and $B$ in a category $\mathcal{C}$, then we obtain unique arrows $u_0:X\rightarrow P$ and $u_1:P\rightarrow X$ which yield the identities $$x_0=p_0\circ u_0,$$ $$p_0=x_0\circ u_1,$$ which we can then substitute into each other to obtain $$x_0=x_0\circ u_1\circ u_0,$$ $$p_0=p_0\circ u_0\circ u_1.$$ At this stage the author asserts that these identities, together with the identities $$x_0=x_0\circ1_X,$$ $$p_0=p_0\circ1_P$$ and the uniqueness condition on $u_0$ and $u_1$ yield the desired equalities $u_0\circ u_1=1_P$ and $u_1\circ u_0=1_X$, but I can't quite see it.

If there is some other arrow $u_2:P\rightarrow X$ such that $u_0\circ u_2=1_P$ then I agree we would have a contradiction, since we then have $$p_0=p_0\circ1_P=p_0\circ u_0\circ u_2=x_0\circ u_2$$ and $u_1$ is unique with this property, but is the existence of $u_2$ necessary if $u_0\circ u_1\neq1_P$? Could the identity not hold and there be no such $u_2$?

(There are of course corresponding identities for $p_1$ and $x_1$, but they lead me to the same question.)

Answer 1

Since $P, p_0,p_1$ is a product diagram, any pair of arrows $C\to A, C\to B$ leads through it by a unique $C\to P$.

Now, for the pair $(x_0,x_1)$ this unique arrow is $u_0:X\to P$, and for the pair $(p_0,p_1)$, it is certainly $1_P$. But, taking the compositions, also $u_0\circ u_1:P\to P$ leads $(p_0,p_1)$ through itself.
This means, by uniqueness, $u_0\circ u_1=1_P$.

Answer 2

This is a way to express the uniqueness property connected with products.

If $P$ serves as product of $A$ and $B$ with projections $p_0:P\to A$ and $p_1:P\to B$ then pair $(p_0,p_1)$ is a so-called monosource which means that on base of the equalities: $$p_0\circ f=p_0\circ g\text{ and }p_1\circ f=p_1\circ g$$ you are allowed to conclude that: $$f=g$$

---

In your case we have: $$p_0\circ u_0\circ u_1=p_0\circ\mathsf{id}_P\text{ and }p_1\circ u_0\circ u_1=p_1\circ\mathsf{id}_P$$ so you are allowed to conclude that: $$u_0\circ u_1=\mathsf{id}_P$$

Similarly it can be found that: $$u_1\circ u_0=\mathsf{id}_X$$ This together proves that $u_0$ and $u_1$ are isomorphisms and are inverses of eachother.