To me it seems that these formulas are not type correct. I think $\mathscr A(A, B)$ is an object of $\mathscr V$, while $FB$ and $GB$ are objects of $\mathscr X$ (and $\otimes$ lives in $\mathscr X$). Can you please clarify?

Thank you very much. I also like these formulas more that the one with the product ($\prod$). The $\prod_{I(x, y)}$ only specifies how the functor under the $\int$ maps objects ($y$); it does not say how this functor maps morphisms.

Thank you; this was very helpful indeed. Lokhorst cites the paper “Linear Logic on Petri Nets” by Engberg and Winskel, which seems to be relevant as well.

So I have to specify what morphisms between adjunctions should be. I think that the canonical answer would be that a morphisms from $F \dashv G$ to $F' \dashv G'$ is a pair of natural transformations $\varphi : F \to F'$ and $\gamma : G \to G'$ such that $\varepsilon' \circ (\varphi \bullet \gamma) = \varepsilon : F \bullet G \to \mathrm{Id}$ and $(\gamma \bullet \varphi) \circ \eta = \eta' : \mathrm{Id} \to G' \bullet F'$. However I do not know how pushouts in 2-categories are defined. Any hints?