Corollary [efr-MUNG]

Let \mathcal {D} be a stochastic module over \mathcal {C}. There is a double category \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {chart} which has decorated spans as its horizontal maps, morphisms in \mathcal {D}|_\mathrm {det} as its vertical maps, and decorated span 2-cells as its 2-cells.

Moreover, there is another double category \widetilde {\mathsf {\mathbb Span}}(\mathcal {D})^\mathrm {lens} which has decorated spans in \mathcal {D}^\mathrm {fop} as its horizontal maps instead.