Pullback functoriality module categories

Theorem 19.2.18 ([Lurie (2017), Theorem 4.5.3.1]). Let \(C\) be a symmetric monoidal \(\infty \)-category. Assume that \(C\) admits geometric realizations and that the tensor product \(\otimes \colon C \times C \to C\) preserves geometric realizations in both variables separately. Then there exists a cocartesian fibration \[ p\colon \Mod (C)^{\otimes } \to \CAlg (C) \times \Span (\Fin ) \] such that for every commutative algebra \(R\) the pullback along \(\{R\} \times \Span (\Fin ) \hookrightarrow \CAlg (C) \times \Span (\Fin )\) is the cocartesian fibration \[ p_R\colon \Mod _R(C)^{\otimes } \to \Span (\Fin ) \] encoding the symmetric monoidal structure on \(\Mod _R(C)\) from Theorem 19.2.14.