Categorical semantics

Definition. A category with representables equipped with open modality (\(\Opn\)-CwR) is a CwR equipped with an idempotent CwR-monad.

Example. Let \(\mc{C} = (\mc{C}_0 \colon \ms{Cat}, \CC_1 \colon \mc{C}_0\op \to \ms{Cat})\) be an indexed category. An indexed presheaf on \(\mc{C}\) consists of \(P_0 \colon \ms{C}_0\op \to \ms{Set}\) along with \(P_1 \colon \left(\int \CC_1 \times P_0\right)\op \to \ms{Set}\). There is a \(\Opn\)-CwR of indexed presheaves where \[\begin{align*} \Opn(P)_0 &= P_0 \\ \Opn(P)_1 &= \ms{const}\,\top \end{align*}\] The notion of representability can be generalized from presheaf categories to indexed presheaf categories; see notes.

Example of example. Let \(\mc{C}_0\) be the category of kind contexts and substitutions in System F\(_\omega\), and \(\CC_1 \colon \mc{C}_0\op \to \ms{Cat}\) be the functor that sends a kind context to the category of type contexts. The classical notion of module (split into a static part, and then a dynamic part which depends on the static part) forms an indexed presheaf on \(\mc{C}\).