Exponential objects of internal objects respecting evaluation (2-exponentials?)

130 Views Asked by At

Let $(F,+_F)$, and $(G,+_G)$ be two commutative internal monoids in Sets. Set being cartesian closed, I can form $G^F$ as a set.

My question is simple: is there a canonical/universal way to enforce that $G^F$ inherits an internal monoidal structure $(G^F, +_{G^F})$ induced by $(F,+_F)$ and $(G,+_G)$ in such a way that it preserves evaluation. That is, in such a way that for all generalized elements $f, g: 1 \rightarrow G^F$, $x, y: 1 \rightarrow F$, $ev \circ (Id \times +_F) \circ (f,x,y) = +_G \circ (ev \times ev)\circ (Id_{G^F} \times \sigma \times Id_F) \circ (\Delta_{G^F} \times Id_F \times Id_F ) \circ (f,x,y)$, where $\sigma$ is the swap (this one means that the elements of the exponential objects are morphism of internal monoids $f(x+_F y) = f(x) +_G f(y)$ ). I also want to impose that it preserves the evaluation: $ev\circ (+_{G^F} \times Id_F) \circ (f,g,x) = +_G \circ (ev \times ev) \circ (Id_{G^F} \times \sigma \times Id_F)\circ (Id_{G^F} \times Id_{G^F} \times \Delta_F) \circ (f,g,x)$, that is in more usual notations $(f+_{G^F}g)(x) = f(x) +_G f(x)$.

Eventually, what I would like to do is to have a 2-sketch of such exponential preserving evaluation objects, that is, a purely syntactic characterization, without having to impose all of the previous equations explicitely: indeed, recalling that an internal monoid in Set (or any other category $\mathcal{C}$) is a functor preserving products from the category of one monoid object to Set, we can see $F$ and $G$ above as two such functors. A natural transformation between the two previous functors being a morphism of monoid, one could always enforce the two required equations above as equations involving different functors preserving products and natural transformations between them in a well chosen 2-category. Obviously, it is already easy to "1-sketch" what it means to an exponential object preserving evaluation by adding everything we want, but this doesn't give me an elegant way to "2-sketch" it without having to enforce all such equations and objects.

I suspect that what I'm looking for is related to the idea of 2-exponential (that is, an exponential that sees further than just the first layer of structure, i.e., it also sees that you have some form of evaluation), but I have no idea if such concepts has already been found/formalized in a satisfying way.