[000I] -- Synthetic topos theory

[000I] Proposition

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. The functor $\mathord {\textnormal {\textsf {E}}}_{C}:{C}^{\mathord {\textnormal {\textsf {op}}}}\rightarrow \mathord {\textnormal {\textsf {LexCocomp}}}(U,V)\backslash C$ is fully faithful.

Proof

Let $$x,y:C$$ be objects. By [000D], the category of morphisms ${y}^{*}\rightarrow {x}^{*}$ in $\mathord {\textnormal {\textsf {LexCocomp}}}(U,V)\backslash C$ is equivalent to the discrete category of morphisms $\mathord {\textnormal {\textsf {1}}}\rightarrow {x}^{*}(y)$ in $$C/x$$ . But the latter is equivalent to the discrete category of morphisms $x\rightarrow y$ in $$C$$ .