The nLab states that a 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.

monoidalnatural transformation, not just a natural transformation. That ought to give the identity you’re after. $\endgroup$ – Dylan Wilson Dec 16 '19 at 14:21equivalentto the data of a strong monoidal structure on the diagonal functor, but I haven't checked this. $\endgroup$ – Tim Campion♦ Dec 16 '19 at 17:05