Theorem [efr-K6NM]

Let \mathcal {C} be any pullback-positive Markov category. Then \mathcal {C}^\to \to \mathcal {C} is a Markov prefibration which thus induces a stochastic module structure on \mathcal {C}^\to |_\mathrm {det}. Writing simply \mathsf {SChart}(\mathcal {C}), \mathsf {SLens}(\mathcal {C}) for \mathsf {SChart}(\mathcal {C}^\to |_\mathrm {det}), \mathsf {SLens}(\mathcal {C}^\to |_\mathrm {det}), we have:

1. There is a functor \mathsf {Optic}(\mathcal {C}) \to \mathsf {SLens}(\mathcal {C}), which is fully faithful. Dually there is a functor \mathsf {coOptic}(\mathcal {C}) \to \mathsf {SChart}(\mathcal {C}) which is fully faithful.
2. \mathsf {SLens}(\mathcal {C}) and \mathsf {SChart}(\mathcal {C}) both admit symmetric monoidal structures, which make the functors \mathsf {SChart}(\mathcal {C}), \mathsf {SLens}(\mathcal {C}) \to \mathcal {C} strict symmetric monoidal, as well as the functors \mathsf {Optic}(\mathcal {C}) \to \mathsf {SLens}(\mathcal {C}), \mathsf {coOptic}(\mathcal {C}) \to \mathsf {SChart}(\mathcal {C}) strong symmetric monoidal.
3. If \mathcal {C} is extensive, this functor preserves the coproducts {A \choose X} + {A \choose Y} = {A \choose X+Y}, and \mathsf {SChart}(\mathcal {C}),\mathsf {SLens}(\mathcal {C}) both admit all finite coproducts.
4. If \mathcal {C} moreover has conditionals and supports, \mathsf {SChart}(\mathcal {C}) = \mathcal {C}^\to