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](https://mathoverflow.net/a/111251), 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](https://math.stackexchange.com/a/4463798/982236). 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.



Proof that the unit of a Cartesian monoidal category is terminal
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.


