Definition Open games in a stochastic module [efr-6I8U]

Let \mathcal {D} be a symmetric monoidal stochastic module fibration over the Markov category \mathcal {C}. Recall that \mathsf {SLens}(\mathcal {D}) acquires a symmetric monoidal structure. Denote as usual \mathsf {SLens}(\mathcal {D})|_\mathrm {det} = \mathsf {SLens}(\mathcal {D}) \times _{\mathcal {C}} \mathcal {C}_\mathrm {det}. Note that this is stable under the monoidal product, and acts on \mathsf {SLens}(\mathcal {D}) via the inclusion.

Then the category of open games in \mathcal {D} is the category \widetilde {\mathsf {Game}} = \mathsf {Para}_{(\mathsf {SLens}(\mathcal {D})|_\mathrm {det})_\mathbb {S}}(\mathsf {SLens}(\mathcal {D})).

When \mathcal {D} \to \mathcal {C} is a Markov prefibration, we overload the notation by writing \widetilde {\mathsf {Game}}(\mathcal {D}) = \mathsf {Game}(\mathcal {D}|_\mathrm {det}).