Definition [efr-98DR]

When \mathcal {C}, \mathcal {D} as above, \widetilde {\mathsf {Game}}(\mathsf {SLens}(\mathcal {D})) acquires a monoidal structure which we call external choice, and write \oplus , given on objects by the coproduct + in \mathsf {SLens}(\mathcal {D}), and on morphisms by the following formula:

Given two open games G_1 = (\overline {\Sigma _A} \otimes \overline {A_1} \to \overline {A_2}, \epsilon _A), G_2 = (\overline {\Sigma _B} \otimes \overline {B_1} \to \overline {B_2}, \epsilon _B), their external choice is has parameter \Sigma _A \& \Sigma _B. The play map is given by (\Sigma _A \& \Sigma _B) \otimes (A_1 + B_1) \cong (\Sigma _A \& \Sigma _B) \otimes A_1 + (\Sigma _A \& \Sigma _B) \otimes B_1 \to \Sigma _A \otimes A_1 + \Sigma _B \otimes B_1 \to A_2 + B_2 The selection relation \epsilon _A \oplus \epsilon _A is given (up to equivalence) as follows: Given a context k: \overline {\Sigma _A} \& \overline {\Sigma _B} \to I, and a deterministic state I \to \overline {\Sigma _A} \& \overline {\Sigma _B}, they are in equilibrium if

1. k factors over the canonical \overline {\Sigma _A} \& \overline {\Sigma _B} \to \overline {\Sigma _A} + \overline {\Sigma _B} for some c: I \to I + I.
2. The factorization being given by k_A, k_B : \overline {\Sigma _A}, \overline {\Sigma _B} \to I ,and I \to \overline {\Sigma _A} \& \overline {\Sigma _B} being given by \sigma _A, \sigma _B : I \to \overline {\Sigma _A}, \overline {\Sigma _B}, we have \epsilon _A(\sigma _A,k_A), \epsilon _B(\sigma _B, k_B)