Let \(U\) be a universe and let \(V\) be a universe strictly greater than \(U\). Then the morphism \({\mathord {\textnormal {\textsf {w}}}}^{*}:{\langle \mathord {\textnormal {\textsf {w}}}\rangle }_{\mathord {\textnormal {\textsf {LexCocomp}}}_{U}}\rightarrow {\langle \mathord {\textnormal {\textsf {w}}}\rangle }_{\mathord {\textnormal {\textsf {LexCocomp}}}_{U}}/\mathord {\textnormal {\textsf {w}}}\) in \(\mathord {\textnormal {\textsf {LexCocomp}}}(U,V)\) is coexponentiable. That is, the pushout functor along \({\mathord {\textnormal {\textsf {w}}}}^{*}\) has a left adjoint.
Proof
By [000G], the pushout along \({\mathord {\textnormal {\textsf {w}}}}^{*}\) is computed by slicing. Since slicing commutes with limits and since the pushout functor commutes with colimits, the adjoint functor theorem applies.