Proof Proof of Theorem [efr-I897] [efr-0BHI]

First recall that \mathsf {Mod}(\mathcal {T},\mathbb {C}) can be identified with the subcategory of [\mathbb {C}^\mathrm {op}, \mathsf {Mod}(\mathcal {T})] spanned by the levelwise representable presheaves. Note that for \mathcal {T} = \mathcal {T}_\mathsf {PsCat}, it suffices to verify representability for C_0,C_1 \in \mathcal {T}_\mathsf {PsCat}, since the rest are pullbacks of these, and pullbacks of representable presheaves are again representable since \mathbb {C} admits pullbacks.

Postcomposition with the previously-constructed functor \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) = \mathsf {Act}(\mathsf {Cat}) \to \mathsf {PsCat}(\mathsf {Act}) = \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) gives a functor [\mathbb {C}^\mathrm {op},\mathsf {Mod}(\mathcal {T}_\mathsf {Act})] \to [\mathbb {C}^\mathrm {op},\mathsf {Mod}(\mathcal {T}_\mathsf {PsCat})]. Clearly this functor preserves representability (again, since limits of representable functors are representable). This gives the desired functor \mathsf {Mod}_s(\mathcal {T}_\mathsf {Act}, \mathbb {C}) \to \mathsf {Mod}_s(\mathcal {T}_\mathsf {PsCat}, \mathbb {C}).

Under the identification of \mathsf {Mod}(\mathcal {T},\mathbb {C}) with a subcategory of [\mathbb {C}^\mathrm {op} \times \mathcal {T}, \mathsf {Cat}], it is clear that the pseudonatural transformations of models correspond to those pseudonatural transformations which are strict on morphisms in \mathbb {C}^\mathrm {op}. This implies the full category \mathsf {Mod}_p(\mathbb {C}) of models and pseudonatural transformations can be identified with the subcategory of [\mathbb {C}^\mathrm {op},\mathsf {Mod}_p(\mathcal {T},\mathsf {Cat})] spanned by those 2-functors which come from models---that is, A: \mathbb {C}^\mathrm {op} \to \mathsf {Mod}_p(\mathcal {T}) = \mathsf {Mod}_p(\mathcal {T},\mathsf {Cat}) must factor over \mathsf {Mod}(\mathcal {T}) \hookrightarrow \mathsf {Mod}_p(\mathcal {T}).

(To be clear: the morphisms in [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T})] are strictly natural transformations between functors \mathbb {C}^\mathrm {op} \to \mathsf {Mod}_p(\mathcal {T}), but each component A(C) \to B(C) of such a natural transformation is a pseudonatural transformation of models).

Under this identification, it is clear that pseudofunctors correspond to those natural transformations in [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T}_\mathsf {PsCat})] which are valued in pseudofunctors, and analogously for pseudolinear morphisms and maps [\mathbb {C}^\mathrm {op}, \mathsf {Mod}_p(\mathcal {T}_\mathsf {Act})]. Hence it suffices to observe that the \mathsf {Cat}-valued version \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) \to \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) carries pseudolinear maps to pseudofunctors.

Note that \mathsf {\mathbb Para}: \mathsf {Mod}(\mathcal {T}_\mathsf {Act}) \to \mathsf {Mod}(\mathcal {T}_\mathsf {PsCat}) is given objectwise as a finite limit. Moreover, since the limit sketch of pseudocategories only involved finite limits, the class of pseudocategories is stable under filtered colimits in [\mathcal {T}_\mathsf {PsCat}, \mathsf {Cat}]. Hence \mathsf {\mathbb Para} commutes with filtered colimits, and is in particular accessible. Hence it admits a left adjoint L (M,C) \mapsto \operatorname {\mathrm {Hom}}_{\mathsf {Mod}(\mathcal {T}_\mathsf {Act})(L(-), (M,C))} where L: \mathcal {T}_\mathsf {PsCat}^\mathrm {op} \to [\mathcal {T}_\mathsf {Act},\mathsf {Cat}] is the restriction of the left adjoint of \mathsf {\mathbb Para}. Both forming the hom-category \operatorname {\mathrm {Hom}}(-, (M,C)) and precomposing with L are 2-functors, and as such preserve pseudonatural transformations. Thus it only remains to observe that \mathsf {\mathbb Para} also preserves the partial strictness property, but this clear.