Criterion for cocartesian morphisms

Proof. The horizontal maps are left fibrations, hence in particular cocartesian fibrations. It follows from closure under base change that also the map from the pullback to \(E_{e/}\) is a cocartesian fibration. By Theorem 23.3.1, the functor \(E_{e'/} \to E_{e/} \times _{C_{pe/}} C_{pe'/}\) is an equivalence if and only if this holds fiberwise over \(E_{e/}\), which means that for every morphism \(\psi \colon e \to e''\) the map \[ \Hom _{E_{e/}}(\phi , \psi ) \to \Hom _{C_{pe/}}(p\phi , p\psi ) \] is an equivalence. Since this is a morphism of animae, this may be checked fiberwise, where it precisely becomes the definition of cocartesianness for \(\phi \). □