Synthetic topos theory
[0053] Definition

Let UU be a universe. We define a functor Q:Cat(U)Topos(U)\mathord {\textnormal {\textsf {Q}}}:\mathord {\textnormal {\textsf {Cat}}}(U)\rightarrow \mathord {\textnormal {\textsf {Topos}}}(U) by Q(C)=C1\mathord {\textnormal {\textsf {Q}}}(C)=C\bullet \mathord {\textnormal {\textsf {1}}}.