nLab monoidal fibration

Definition

A monoidal fibration is a functor $\Phi\colon E\to B$ such that

• $\Phi$ is a Grothendieck fibration

• $E$ and $B$ are monoidal categories and $\Phi$ is a strict monoidal functor, and

• the tensor product of $E$ preserves cartesian arrows.

If $B$ is cartesian monoidal, then monoidal fibrations over $B$ are equivalent to pseudofunctors $B^{op} \to MonCat$, which are called indexed monoidal categories. In this case the tensor product on $E$ is the external tensor product of the indexed monoidal category.

Related concepts

• indexed monoidal category, dependent linear type theory

• monoidal Grothendieck construction

References

• Mike Shulman, Framed bicategories and monoidal fibrations, TAC