Synthetic topos theory
[000X] Proposition

Let UU be a universe and let VV be a universe strictly greater than UU. Then the morphism w:wLexCocompUwLexCocompU/w{\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 LexCocomp(U,V)\mathord {\textnormal {\textsf {LexCocomp}}}(U,V) is a co-left-fibration.

Proof

This follows from [000D] because, for any lex UU-cocomplete category CC, the projection (F:LexCocompU(wLexCocompU,C))×(1F(w))LexCocompU(wLexCocompU,C)(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.