Definition [efr-1WGM]

Let \mathcal {C} be a semiCartesian symmetric monoidal category. The symmetric monoidal double category of open games in \mathcal {C} is \widetilde {\mathsf {Game}}(\mathcal {C}) = \mathsf {\mathbb Para}_{\mathsf {Optic}(\mathcal {C})_\mathbb {S}}(\mathsf {Optic}(\mathcal {C})).