The Double Category of Stochastic Arenas [efr-001L]

Let \mathcal {D} \to \mathcal {C}_\mathrm {det} be a Markov fibration. Since it is a fibration, we may form the ordinary double category of arenas \mathsf {\mathbb Arena}(\mathcal {D}). Note that there is a double functor \mathsf {\mathbb Arena}(\mathcal {D}) \to \mathcal {C}_\mathrm {det}^\square . This is a double fibration: an internal category in the category of fibrations.

The double category of stochastic arenas is obtained by stochastically completing this fibration in both directions---in other words, we form the completions \overline {\mathsf {\mathbb Arena}(\mathcal {D})_1} and \overline {\mathsf {\mathbb Arena}(\mathcal {D})_2}. We must check that this still gives a double category (it does), which we then transpose, stochastically complete, then transpose again (once again, there is something to check to see that the completion preserves the double categorical structure).

The phrase "stochastic arenas" is a bit unfortunate, since the arenas themselves are no different from ordinary arenas (stochastic completion does not change the objects). Rather, it is the morphisms, the lenses and charts, that are stochastic.