Evaluation as a cocartesian functor

Proof. Recall from Example 23.1.10 that the target functor \(t\colon \Ar (C) \to C\) is a cocartesian fibration whose cocartesian morphisms are those squares inverted by \(s\colon \Ar (C) \to C\). The projection functor \(\pr _2\) is cocartesian by Lemma 23.1.13, and its cocartesian morphisms are those pairs \((g\colon X \to X', f\colon Y\to Y')\) such that \(g\) is an isomorphism. It follows immediately from these descriptions that \((s,t)\) is a cocartesian functor. □