Terminal objects via source maps

Proof. We only prove (1); the case of (2) is dual. If \(C_{/x} \to C\) is an equivalence, then it follows from Corollary 21.3.3 that \(x\) is terminal in \(x\), as it is the image under this equivalence of the terminal object \((x,\id _x) \in C_{/x}\). So assume that \(x\) is a terminal object. By Remark 21.2.3, this means that the functor \(x\colon * \to C\) is a right adjoint to \(p_C\colon * \to C\), and in particular there is a natural transformation \(\epsilon \colon \id _C \to \const _x\) satisfying the triangle identity. We may now construct a functor \[ \phi \colon C \to C_{/x}, \qquad y \mapsto (y, \epsilon _y\colon y \to x). \] More precisely, we may think of \(\epsilon \) as a functor \(\overline {\epsilon }\colon C \to \Ar (C)\), and since the target of \(\epsilon \) is \(\const _x\) we see that \(\overline {\epsilon }\) canonically factors through the slice \(C_{/x}\). It is also clear from this definition that we have \(s \circ \phi \cong \id _C\). It remains to show that we also have \(\phi \circ s \cong \id _{C_{/x}}\).

The functor \(\overline {\epsilon }\colon C \to \Ar (C)\) induces a functor \(\overline {\epsilon }_*\colon \Ar (C) \to \Fun ([1] \times [1],C)\), which informally speaking sends a morphism \(f\colon y \to z\) to the ‘naturality square’ induced by \(\epsilon \):

Note that for \(z = x\), it follows from the triangle identities for the adjunction that the map \(\epsilon _x\colon x \to x\) is the identity map. So restricting the naturality square to objects of the form \((y,f) \in C_{/x}\), this square takes the form

This shows that the object \((y,f)\) of \(C_{/x}\) is naturally isomorphic to \((y, \epsilon _y\colon y \to x)\), producing the desired natural isomorphism \(\phi \circ s \cong \id _{C/x}\). □