The [nLab](https://ncatlab.org/nlab/show/semicartesian+monoidal+category) states that a [semicartesian monoidal category](https://ncatlab.org/nlab/show/semicartesian+monoidal+category) equipped with natural transformations $\delta\_x : x \to x \otimes x$ such that $\pi\_1 \circ \delta\_x = 1\_x$ and $\pi\_2 \circ \delta\_x = 1\_x$ (where $\pi\_1$ and $\pi\_2$ are the definable projections), is automatically cartesian.


I'm looking for a proof of this statement.


I managed to show that given $f\_1 : a \to b\_1$ and $f\_2 : a \to b\_2$, we can construct a map $(f\_1, f\_2) : a \to b\_1 \otimes b\_2$ as $(f\_1, f\_2) = (f\_1 \otimes f\_2) \circ \delta\_a$, and this map projects appropriately:
\begin{equation}
 \pi\_i \circ (f\_1 \otimes f\_2) \circ \delta\_a = f\_i \circ \pi\_i \circ \delta\_a = f\_i.
\end{equation}


Now I'm trying to show that $(f\_1, f\_2)$ is the unique map with this property. However, I seem to require that $(\pi\_1 \otimes \pi\_2) \circ \delta\_{x \otimes y} = 1\_{x \otimes y}$. Then if there is another function $h : a \to b\_1 \otimes b\_2$ such that $\pi\_i \circ h = f\_i$, we have
\begin{equation}
 h = (\pi\_1 \otimes \pi\_2) \circ \delta\_{b\_1 \otimes b\_2} \circ h
 = (\pi\_1 \otimes \pi\_2) \circ (h \otimes h) \circ \delta\_a = (f\_1 \otimes f\_2) \circ \delta\_a = (f\_1, f\_2).
\end{equation}
Is it correct that we need to postulate this "$\eta$-equality"? I have an intuition that it may somehow follow from the unit laws (since it already holds if either $x$ or $y$ is the terminal object), but I don't know how to prove that.



A semicartesian monoidal category with diagonals is cartesian: proof?
As pointed out by Dylan Wilson, the nLab postulates that $\delta$ be a monoidal natural transformation. This requires that the functor $Gx = x \otimes x$ be a (lax/oplax) monoidal functor. Let us assume that the category is symmetric monoidal, then $G$ is strong (in the sense of non-lax) monoidal. Then we have an isomorphism
\begin{equation}
 \iota : G(x \otimes y) = (x \otimes y) \otimes (x \otimes y) \cong (x \otimes x) \otimes (y \otimes y) = Gx \otimes Gy
\end{equation}
Of course the symmetric structure provides multiple such morphisms, but naturality w.r.t. $x \to \top$ and $y \to \top$ implies that $\pi\_i \circ \iota = G\pi\_i = \pi\_i \otimes \pi\_i$, which reveals that $\iota$ swaps the middle two components, and hence $\pi\_1 \otimes \pi\_2 = (\pi\_1 \otimes \pi\_2) \circ \iota$.


Then we have
\begin{align\*}
(\pi\_1 \otimes \pi\_2) \circ \delta\_{x \otimes y}
&= (\pi\_1 \otimes \pi\_2) \circ \iota \circ \delta\_{x \otimes y} \\
&= (\pi\_1 \otimes \pi\_2) \circ (\delta\_x \otimes \delta\_y) \\
&= (1 \otimes 1) = 1,
\end{align\*}
proving the equation that was missing in the question.


