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.

butthe tensor product is not the product. These are calledsemicartesian monoidal categories. See the nlab page ncatlab.org/nlab/show/semicartesian+monoidal+category as well as golem.ph.utexas.edu/category/2016/08/… for a discussion on these. $\endgroup$