We have one argument automatically, let's do the other. One approach:
If we have (A -> B), to give C^B -> C^A, it's equivalent to give A C^B -> C, for which it suffices to give B C^B -> C, which we (should) have.
I think this would be easier to prove things about if we use the unit/counit parts of adjunction (the middle step I gave is natural, which we also might need to add - we need that prodinl is natural in X).
Might also involve #14.
b-mehta
commented
4 years ago
We have one argument automatically, let's do the other. One approach: If we have (A -> B), to give C^B -> C^A, it's equivalent to give A C^B -> C, for which it suffices to give B C^B -> C, which we (should) have. I think this would be easier to prove things about if we use the unit/counit parts of adjunction (the middle step I gave is natural, which we also might need to add - we need that
prodinlis natural inX). Might also involve #14.