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.

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.