Synthetic topos theory
[000F] Definition

Let \(U\) be a universe. We define \({\langle \mathord {\textnormal {\textsf {w}}}\rangle }_{\mathord {\textnormal {\textsf {LexCocomp}}}_{U}}\) to be the free lex \(U\)-cocomplete category generated by one object \(\mathord {\textnormal {\textsf {w}}}\). That is, for any lex \(U\)-cocomplete category \(C\), the functor

\(F\mapsto F(\mathord {\textnormal {\textsf {w}}}):\mathord {\textnormal {\textsf {LexCocomp}}}_{U}({\langle \mathord {\textnormal {\textsf {w}}}\rangle }_{\mathord {\textnormal {\textsf {LexCocomp}}}_{U}},C)\rightarrow C\)
is an equivalence.