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 a co-left-fibration.
Proof
This follows from [000D] because, for any lex \(U\)-cocomplete category \(C\), the projection \((F:\mathord {\textnormal {\textsf {LexCocomp}}}_{U}({\langle \mathord {\textnormal {\textsf {w}}}\rangle }_{\mathord {\textnormal {\textsf {LexCocomp}}}_{U}},C))\times (\mathord {\textnormal {\textsf {1}}}\rightarrow F(\mathord {\textnormal {\textsf {w}}}))\rightarrow \mathord {\textnormal {\textsf {LexCocomp}}}_{U}({\langle \mathord {\textnormal {\textsf {w}}}\rangle }_{\mathord {\textnormal {\textsf {LexCocomp}}}_{U}},C)\) is a left fibration.