[000D] -- Synthetic topos theory

[000D] Proposition

Let $$U$$ be a universe, let $$C$$ be a lex $$U$$ -cocomplete category, and let $$x:C$$ be an object. Then the pair $({x}^{*},\mathord {\textnormal {\textsf {d}}}_{x})$ has the following universal property: For any lex $$U$$ -cocomplete category $$D$$ , the equivalence given in [000C] restricts to an equivalence

\mathord {\textnormal {\textsf {LexCocomp}}}_{U}(C/x,D)\simeq (F:\mathord {\textnormal {\textsf {LexCocomp}}}_{U}(C,D))\times (\mathord {\textnormal {\textsf {1}}}\rightarrow F(x))

Proof

This follows from the fact that, for any lex $$U$$ -cocomplete category $$C$$ and any morphism $u:x\rightarrow y$ in $$C$$ , the pullback functor ${u}^{*}:C/y\rightarrow C/x$ is a morphism of lex $$U$$ -cocomplete categories.