Lemma 23.1.7 (Uniqueness of cocartesian lifts). For a functor \(p\colon E \to C\), consider the full subcategory \[ \Ar ^{\textup {cocart}}(E) \subseteq \Ar (E) \] spanned by the \(p\)-cocartesian morphisms. The functor \[ \Ar ^{\textup {cocart}}(E) \to \Ar (C) \times _{s,C,p} E , \quad (\phi \colon e \to e') \mapsto (p\phi , e) \] is fully faithful. It is an equivalence if and only if \(p\) is a cocartesian fibration.
Proof. Set \(B:=\Ar (C)\times _{s,C,p}E\), and let \(B^{\mathrm {lift}}\subseteq B\) be the full subcategory spanned by the pairs \((f,e)\) that admit a cocartesian lift. By Lemma 23.1.2, Lemma 21.1.4, these lifts assemble into a left adjoint \[ L\colon B^{\mathrm {lift}}\longrightarrow \Ar (E)\times _B B^{\mathrm {lift}} \] to the projection. Its unit is an equivalence, so \(L\) is fully faithful. Its essential image is precisely \(\Ar ^{\textup {cocart}}(E)\), since the cocartesian arrows are exactly the left adjoint objects described in Lemma 23.1.2. Thus the displayed functor identifies with the inclusion \(B^{\mathrm {lift}}\hookrightarrow B\). It is therefore fully faithful, and it is an equivalence precisely when every pair \((f,e)\) admits a cocartesian lift. □
Generated from the authoritative LaTeX source.