Example Decorated \mathsf {Para} [efr-AIT8]

Let \mathcal {C} be symmetric monoidal, and let S: \mathcal {C} \to \mathsf {Set} be a symmetric lax monoidal functor. Then the category of elements \int _\mathcal {C} S = \{(X \in \mathcal {C}, s \in S(X))\} acquires a symmetric monoidal structure (with the laxator and unitor giving the multiplication on the elements s), so that the obvious forgetful functor \int _\mathcal {C} S \to \mathcal {C} is symmetric.

With the action \int _\mathcal {C} \curverightarrow \mathcal {C} induced by this functor, the (horizontal) morphisms of \mathsf {\mathbb Para}_{\int \mathcal {C}}(\mathcal {C}) are parametrized morphisms P \otimes X \to Y equipped with an element of S(P), and the 2-cells are reparametrization morphisms which preserve the decoration. This may be denoted \mathsf {\mathbb Para}_S(\mathcal {C})