Synthetic topos theory
[000C] Exercise

Let \(C\) be a category that has finite limits and let \(x:C\) be an object. Then the pair \(({x}^{*},\mathord {\textnormal {\textsf {d}}}_{x})\) has the following universal property: For any category \(D\) that has finite limits, the functor

\(G\mapsto (G\circ {x}^{*},G(\mathord {\textnormal {\textsf {d}}}_{x})):\mathord {\textnormal {\textsf {Lex}}}(C/x,D)\rightarrow (F:\mathord {\textnormal {\textsf {Lex}}}(C,D))\times (\mathord {\textnormal {\textsf {1}}}\rightarrow F(x))\)
is an equivalence. Moreover, the inverse of this functor at \((F,u)\) is \({u}^{*}\circ (F/x)\).