Synthetic topos theory
[0010] Definition

Let \(U\) be a universe, let \(V\) be a universe strictly greater than \(U\), and let \(C\) be a \(V\)-small lex \(U\)-cocomplete category. We define a functor

\(\mathord {\textnormal {\textsf {E}}}_{C}:{C}^{\mathord {\textnormal {\textsf {op}}}}\rightarrow \mathord {\textnormal {\textsf {LexCocomp}}}(U,V)\backslash C\)
by \(\mathord {\textnormal {\textsf {E}}}_{C}(x)=({x}^{*}:C\rightarrow C/x)\).