Skip to main content
Source Link
Samuel Reid
  • 1.4k
  • 11
  • 23

Adjoint of Pushout as Modal Operators in Internal Logic

Regarding the internalization of mathematics to a particular category as in the nLab article: Internal Logic, there is a peculiar table mentioned in the section on Categorical Semantics 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?