In \$$R\vdash L\$$ we need a natural bijection between \$$$L(a),b$ \leftrightarrow $a,R(b)$\$$.

Okay so looking at the bijection's two sides for the left adjoint of \$$\times\$$ \$[L(X),(S,T)] \leftrightarrow [X,S \times T]\$, which requires \$|S|^{|L_0(X)|} \ast |T|^{|L_1(X)|} = (|S|\ast|T|)^{|X|}\$

Setting those equal and using that it has to work for all \$$X\$$ , we get \$$L_0(X)=L_1(X)=X\$$.

So L must be equivalent to the diagonal/duplication/\$$\delta\$$ and I am going to take Johns advice and just assume that if I make L _be_ \$$\delta\$$ then it ends up being natural. (My in my head calculations/gut feel says its plausible at least)

so the bijection has type [(X,X),(S,T)] <-> [X,S x T], and the forward direction is basically just the pair (term) constructor, so yeah it's natural and a bijection. (I know this because of some programming language theory stuff and a little bit of hand waving. This is an engineers approach not a mathematician's)

Now I have a hunch here. Let's see if it's also the *right* adjoint of *+* !

[S+T,X] <-> [(S,T),(X,X)] is the type of the bijection we need.
And yeah, the back direction is (basically) just definition by cases which better be a natural bijection. (for the same reasons as the above.)

We can use some algebra and prove that the right adjoint must be equivalent to \$$\delta\$$ the same way as above. So this forms an adjoint triplet \$$\times \vdash \delta \vdash +\$$, which I think we saw forall, there exists, and ..something forming back when we were working with preorders.