Proving basic lemmas about categories with finite products and terminal/initial objects. I would expect that in any category $\mathcal{C}$ with finite products and a terminal object $1$, the isomorphism $X \times 1 \cong X$ should hold, but I have a rather hard time finding the proof of this.
In my attempt, I use the fact that there are arrows $1_X : X \rightarrow X$ and $\top_X : X \rightarrow 1$, from which the universal property of $X \times 1$ gives me a unique $u : X \rightarrow X \times 1$ such that $\pi_1 \circ u = 1_X$ (and $\pi_2 \circ u = \top_X$). This gets me halfway, but I still need to prove that $u \circ \pi_1 = 1_{X \times 1}$ to prove that $u$ is indeed an iso.
I can easily obtain that $\pi_1 \circ u \circ \pi_1 = \pi_1 = \pi_1 \circ 1_{X \times 1}$, so as far as I can see, the problem can be reduced to proving that $\pi_1$ is a mono.
However, how to get there? Is this even provable, or do I need extra assumptions about $\mathcal{C}$? If it is provable, would $X \times 0 \cong 0$ be provable as well (assuming initial objects)?
Thanks!
 A: While I was writing, a proof was submitted.  So I'll submit the following non-rigorous exposition, which will hopefully be good for some intuition.
Yes, this is true.  we can see from quite general principles that it must be true, without working out any details: the identity is a limit, and the terminal object is a limit, and products are a limit.  And limits commute; that is, it doesn't matter what order you compute them in, or whether you compute them in pieces or all at once.
(By the way, I'll use $\bullet$ instead of $1$ for now—$1$ is good notation but I don't want to get confused with the identity morphisms)
You are trying to calculate the limit of the diagram $X\to \bullet$ in two different ways.  First, by simply taking $X$ itself as the limit diagram—then there is of course a unique way to add the map to $\bullet$.  And second, by beginning with $\bullet$, then adding $X$ to your limit diagram.  These must give the same answer, if category theory is to work right.
Getting a little more technical: Let's fix some $Y$ and look at the set $\operatorname{Hom}(Y,X\times \bullet)$.  A map to a product is the same thing as a pair of maps, and so an element of this set is a map $Y\to X$, and map $Y\to\bullet$.  But the latter is unique—so we have shown that $\operatorname{Hom}(Y,X\times \bullet)=\operatorname{Hom}(Y,X)$.
Actually, that's already a proof, if we are comfortable with the Yoneda embedding.  But even if not, it gives us a few big hints on how to proceed, since it gives us a nice dictionary between the two objects.
Take the identity map $1_X : X\to X$.  As we observed, this has a natural friend $\psi: X\to X\times \bullet$, which is $\psi = id_X \times u_X$, where $u_X : X\to \bullet$ is the unique map.  It is reasonable to guess that it is an isomorphism.  And it is also reasonable to guess that the inverse is the only map we can think of in the other direction, which is the projection $\pi: X\times \bullet \to X$.
A: To show that $u \circ \pi_1 = id$ consider that $u \circ \pi_1$ is a morphism from $X\times 1 \to X\times 1$ such that $\pi_1 \circ u \circ \pi_1 = \pi_1$ and $\top_{X\times 1} = \top_{X\times 1} \circ u \circ \pi_1$. Since these equations also hold if you replace $u \circ \pi_1$ by $1_{X\times 1}$, you get by uniqueness that $u \circ \pi_1 = 1_{X\times 1}$. 
The property $X \times 0 = 0$ does not hold in general. Consider the category of groups, where $1 = 0$, so $X \times 1 = X$ and since there are nontrivial groups the property clearly doesn't hold.
The property does however hold if, for instance, the category is cartesian closed.
