Theorem [efr-I897]

Let \mathbb {C} be a 2-category which admits pullbacks, products and comma objects. Then there is a functor \mathsf {\mathbb Para}: \mathsf {Act}(\mathbb {C}) \to \mathsf {PsCat}(\mathbb {C}) from the 2-category of pseudomonoid actions and pseudolinear maps to the 2-category of pseudocategories and pseudofunctors, with \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_0 = \mathcal {C} and \mathsf {\mathbb Para}_\mathcal {M}(\mathcal {C})_1 = \mathcal {M} \times \mathcal {C} \downarrow \mathcal {C}. This functor preserves strict maps, limits, and filtered colimits.