Regarding the internalization of mathematics to a particular category as in the nLab article: [Internal Logic][1], there is a peculiar table mentioned in the section on [Categorical Semantics][2] in which there is a corresponding category-theoretic construction to the regular logical operators in a theory. In particular, $\wedge$ corresponds to a pullback of a cospan, $\top$ corresponds to the top element (A itself), $\wedge$ corresponds to union, $\bot$ corresponds to the bottom element (strict initial object), $\Rightarrow$ corresponds to the Heyting implication, $\exists$ corresponds to the left adjoint to a pullback (I'm not sure which pullback in particular?), and $\forall$ corresponds to the right adjoint to a pullback (what pullback is this also?).

Would it be possible to define the modal operators of $\Box$ and $\Diamond$ as the right adjoint of a pushout (similarly to how $\forall$ is the right adjoint to a pullback) and the left adjoint of a pushout (similarly to how $\exists$ is the left adjoint to a pullback), respectively? Or, if this does not work, could it be possible to define modal operators in internal logic using some other category theoretic construction?

  [1]: http://ncatlab.org/nlab/show/internal+logic
  [2]: http://ncatlab.org/nlab/show/internal+logic#CategoricalSemantics