Synthetic topos theory
[000G] Proposition

Let \(U\) be a universe, let \(V\) be a universe strictly greater than \(U\), let \(C\) be a \(V\)-small lex \(U\)-cocomplete category, and let \(x:C\) be an object. Let \(F:{\langle \mathord {\textnormal {\textsf {w}}}\rangle }_{\mathord {\textnormal {\textsf {LexCocomp}}}_{U}}\rightarrow C\) denote the morphism of lex \(U\)-cocomplete categories corresponding to \(x\). Then \({x}^{*}:C\rightarrow C/x\) is the pushout in \(\mathord {\textnormal {\textsf {LexCocomp}}}(U,V)\) of \({\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}}}\) along \(F\).

Proof

One can check the universal property of the pushout using [000D].