Corollary [efr-UI90]

Since \mathbb {S} is lax monoidal, its Grothendieck construction \int \mathbb {S}_\mathcal {C} acquires a monoidal structure (Reference [moeller-vasilakopoulou]). We write this category \mathcal {C}_\mathbb {S}---explicitly, it is given as follows:

1. The objects are pairs (X,\epsilon ) where X \in \mathcal {C} and \epsilon \in \mathbb {S}(X) is a selection relation on it
2. The morphisms are morphisms f: X \to Y so that, for every x: I \to X, k: Y \to I, \epsilon (x, kf) \Rightarrow \epsilon (fx, k)
3. The monoidal structure is given by (X,\epsilon ) \otimes (Y,\epsilon ') = (X \otimes Y, \epsilon \boxtimes \epsilon ')