Proposition [efr-JD5V]

Let \mathcal {C} be any 2-category. Consider the 2-category \mathsf {PsCat}(\mathcal {C})_{\mathrm {ps},\mathrm {nm}} of pseudocategories, normal pseudofunctors and natural transformations in \mathcal {C}.

1. For every X \in \mathcal {C}, there is a functor (-)^X: \mathsf {PsCat}(\mathcal {C}) \to \mathsf {PsCat}(\mathsf {Cat}) which simply applies (-)^X to all the data of the internal pseudocategory. This is contravariant functorial in X.
2. If \mathcal {C} has finite strict 2-limits, for every finite pseudo double category K there is a functor (-)^K: \mathsf {PsCat}(\mathcal {C})_\mathrm {ps} \to \mathcal {C} defined by the universal property that \mathcal {C}(A,C^K) \cong \mathsf {PsCat}(\mathsf {Cat})(K,C^A)