[000X] PropositionLet UUU be a universe and let VVV be a universe strictly greater than UUU. Then the morphism w∗:⟨w⟩LexCocompU→⟨w⟩LexCocompU/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}}}w∗:⟨w⟩LexCocompU→⟨w⟩LexCocompU/w in LexCocomp(U,V)\mathord {\textnormal {\textsf {LexCocomp}}}(U,V)LexCocomp(U,V) is a co-left-fibration.ProofThis follows from [000D] because, for any lex UUU-cocomplete category CCC, the projection (F:LexCocompU(⟨w⟩LexCocompU,C))×(1→F(w))→LexCocompU(⟨w⟩LexCocompU,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)(F:LexCocompU(⟨w⟩LexCocompU,C))×(1→F(w))→LexCocompU(⟨w⟩LexCocompU,C) is a left fibration.