A semicartesian monoidal category with diagonals is cartesian: proof? 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.
 A: 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.
