Here's a blow-by-blow proof of the "super-theorem" (**Puzzle 83**):

First, note that \\(f\\) left adjoint to \\(g\\) implies that \\((fx \leq y \iff x \leq gy)\\) and that \\(fgy \leq y\\)

Now assume \\(f\\) is oplax monoidal.

The adjunction immediately gives us \\(f1_X \leq 1_Y \implies 1_X \leq g1_Y\\)

As for the product rule, we have \\(f(x_0 \otimes x_1) \leq fx_0 \otimes fx_1\\)

So by adjunction we get \\(x_0 \otimes x_1 \leq g(fx_0 \otimes fx_1)\\)

Setting \\(x_0 = gy_0\\) and \\(x_1 = gy_1\\), we get \\(gy_0 \otimes gy_1 \leq g(fgy_0 \otimes fgy_1)\\)

But \\(fgy_0 \leq y_0\\) and \\(fgy_1 \leq y_1\\), so \\(fgy_0 \otimes fgy_1 \leq y_0 \otimes y_1\\)

And \\(g\\) is monotone, so \\(g(fgy_0 \otimes fgy_1) \leq g(y_0 \otimes y_1)\\)

Putting these together we get \\(gy_0 \otimes gy_1 \leq g(y_0 \otimes y_1)\\)

So \\(g\\) is lax monoidal.

The converse (\\(g\\) lax \\(\implies\\) \\(f\\) oplax) follows by duality.

First, note that \\(f\\) left adjoint to \\(g\\) implies that \\((fx \leq y \iff x \leq gy)\\) and that \\(fgy \leq y\\)

Now assume \\(f\\) is oplax monoidal.

The adjunction immediately gives us \\(f1_X \leq 1_Y \implies 1_X \leq g1_Y\\)

As for the product rule, we have \\(f(x_0 \otimes x_1) \leq fx_0 \otimes fx_1\\)

So by adjunction we get \\(x_0 \otimes x_1 \leq g(fx_0 \otimes fx_1)\\)

Setting \\(x_0 = gy_0\\) and \\(x_1 = gy_1\\), we get \\(gy_0 \otimes gy_1 \leq g(fgy_0 \otimes fgy_1)\\)

But \\(fgy_0 \leq y_0\\) and \\(fgy_1 \leq y_1\\), so \\(fgy_0 \otimes fgy_1 \leq y_0 \otimes y_1\\)

And \\(g\\) is monotone, so \\(g(fgy_0 \otimes fgy_1) \leq g(y_0 \otimes y_1)\\)

Putting these together we get \\(gy_0 \otimes gy_1 \leq g(y_0 \otimes y_1)\\)

So \\(g\\) is lax monoidal.

The converse (\\(g\\) lax \\(\implies\\) \\(f\\) oplax) follows by duality.