By Reference [moeller-vasilakopoulou], \mathsf {MonFib}(\mathcal {C}_\mathrm {det}) is equivalent to the category of pseudomonoids in \mathsf {Fib}(\mathcal {C}_det). Since the monad preserves products, it must preserve pseudomonoids, which is all we need.

Now suppose \mathcal {D} \to \mathcal {C} is a monoidal prefibration. Then its underlying fibration is a monoidal fibration, hence an object of \mathsf {MonFib}(\mathcal {C}_\mathrm {det}). The claim is that the functor \overline {\mathcal {D}|_\mathrm {det}}|_\mathrm {det} \to \mathcal {D}|_\mathrm {det} is monoidal. The induced monoidal structure is given on objects by \otimes _\mathcal {D} and takes a pair of morphisms in the fiber represented by sections (s: X \to M, \phi : \bar {X_0}_M) \to \bar {X_1}_M and s': X \to M', \phi ': \bar {X'_0}_M \to \bar {X'_1}_M to \langle s,s' \rangle : X \to M \times _X M', \pi _M^*\phi \otimes _\mathcal {D} \pi _{M'}^*\phi '. Recalling that the algebra structure is defined by taking (s,\phi ) to the composite \bar {X_0} \to \bar {X_0}_M \xrightarrow {\phi } \bar {X_1}_M \to \bar {X_1}, and chasing the below diagram around, it is apparent that the algebra structure preserves the monoidal structure.

Now let \mathcal {D}_0 be a monoidal stochastic module in this sense. It suffices to show that the free prefibration \overline {\mathcal {D}_0} is a monoidal prefibration, by Lemma [efr-7GH5], and the induced functor \mathsf {SChart}(\mathcal {D}_0) \to \mathcal {C} will clearly be strict monoidal if \overline {\mathcal {D}_0} \to \mathcal {C} is.

To construct this monoidal structure on \mathcal {D}_0, simply note that since \overline {(-)} preserves global limits as well, there is an induced monoidal structure on \overline {\mathcal {D}_0} so that the forgetful functor is strict monoidal. Recalling that the Cartesian lifts of f: X \to Y \in \mathcal {C} to \overline {\mathcal {D}_0} are given by the span X = X \to Y and the morphism 1_{f^*\bar {Y}}, it is easy to see by unwinding the definition that these are stable under tensor.

If \mathcal {D}_0 has weak supports, we have already proven that \mathsf {SChart}(\mathcal {D}_0) \to \mathcal {C} is a strict monoidal functor, and weak supports are equivalent to the claim that it is a prefibration. Since the Cartesian lifts are just the equivalence classes of the Cartesian lifts in \overline {\mathcal {D}_0}, the preceding claim that they are stable under tensor implies the same for \mathsf {SChart}(\mathcal {D}_0), finishing the proof.

The last point is mostly trivial. The product preservation still establishes the lifting to \mathsf {BrMonFib}(\mathcal {C}_\mathrm {det}) and \mathsf {SymMonFib}(\mathcal {C}_\mathrm {det}). Given a braided or symmetric monoidal prefibration, the braidings are Cartesian and in the deterministic part, so the underlying fibration is braided/symmetric and they are preserves by the stochastic module structure. The braiding/symmetry on \mathsf {SChart} follows again from Lemma [efr-7GH5], and there is nothing to show for the last point.