Proof that the unit of a Cartesian monoidal category is terminal

Question

In short, given a monoidal category whose product is the categorical product, show that the unit object is terminal.

This looks very similar to questions that have been answered, but is subtly different - much of the relevant literature discusses how categories with binary products and a terminal object admit a monoidal structure. This was proved in this post, for instance. I, however, am asking whether the binary products and monoidal structure imply the terminality of the unit.

Furthermore, this has been proved if the existence of a terminal object in the category is known here. But how can we deduce it without using the existence of a terminal object? Or, therefore equivalently, can we deduce the existence of a terminal object from the monoidal category and product axioms?

I am quite confident the statement is true given how interchangeably and loosely the two distinct concepts are used throughout the literature... of course, if it is not true, is there a monoidal category with categorical product whose unit isn't terminal?

So far...: Let the category in consideration be $(\mathcal{C},\times,I,\lambda, \rho, \alpha)$. So far, I have been able to reduce the problem to showing that there is only one morphism $I\times I\to I$ through the following argument:

If there is only one map $I\times I\to I$, it must be $\lambda_I\equiv\lambda$. For the object $I\times I$, both projections are thus $\lambda$; for any $A\in\mathcal{C}$, given any two $f,g\colon A\to I$, the definition of a categorical product gives us that $\exists !u\colon A\to I\times I$ such that $f=\lambda\circ u$ and $g=\lambda\circ u$, and thus $f=g$, so there is only one $A\to I$. (In reality, we actually only need the show that the two projections of the object $I\times I$ are identical.)

Thank you very much for any guidance on this problem. To reiterate, one could show any of the following equivalent statements:

(0) $I$ is terminal.

(1) $\mathcal{C}$ must have some terminal object.

(2) The projection maps for $I\times I$ are equal.

Answer 1

Here is a down-to-earth answer.

For ease of notation, let $\lambda: A\to I\times A$ be the component of the unitor and let $\pi_1$ and $\pi_2$ be the projections from $I\times A$ to $I$ and $A$.

Then we have (in sets):

$$\mathrm{Hom}(A,A)\cong_{\lambda_*} \mathrm{Hom}(A,I\times A) \cong_{(\pi_1)_*, (\pi_2)_*} \mathrm{Hom}(A,I) \times \mathrm{Hom}(A,A). $$ That is, a morphism $f:A\to A$ is taken by this isomorphism to $(\pi_1 \lambda f, \pi_2\lambda f)$. By naturality of $\lambda$ the first component $\pi_1\lambda f$ is the same as $\pi_1 (1_I \times f)\lambda$. In turn, by properties of the product, this is $\pi_1 \lambda$. Specifically, it is independent of $f$.

So we have that the map $\mathrm{Hom}(A,A)\to \mathrm{Hom}(A,I) \times \mathrm{Hom}(A,A)$ given by $$ f \mapsto \left((\pi_1\lambda), (\pi_2\lambda f)\right) $$ is an isomorphism. If $\mathrm{Hom}(A,I)$ has any element other than $\pi_1\lambda$, this would not be surjective.