Monoidal Grothendieck construction

Understand

We lift the standard equivalence between fibrations and indexed categories to an equivalence between monoidal fibrations and monoidal indexed categories, namely weak monoidal pseudofunctors to the 2-category of categories.

• In doing so, we investigate the relation between this `global' monoidal structure where the total category is monoidal and the fibration strictly preserves the structure, and a `fibrewise' one where the fibres are monoidal and the reindexing functors strongly preserve the structure, first hinted by Shulman.
• In particular, when the domain is cocartesian monoidal, lax monoidal structures on the functor to the 2-category of categories correspond to lifts of the functor to the 2-category of monoidal categories.
• Finally, we give examples where this correspondence appears, spanning from the fundamental and family fibrations to network models and systems.