Characterizations of left fibrations

Proof. It is clear that (1) implies (2): every morphism in the fiber \(E_x\) is sent to the identity morphism \(\id _x\), hence is an isomorphism by conservativity of \(p\).

Assuming (2), consider a morphism \(\psi \colon e \to e''\) in \(E\). We need to show that \(\psi \) is \(p\)-cocartesian. Since \(p\) is a cocartesian fibration, there exists a \(p\)-cocartesian morphism \(\phi \colon e \to e'\) lifting \(p(\psi )\). Since \(\phi \) is \(p\)-cocartesian, there then exists a unique morphism \(\xi \colon e' \to e''\) fitting in the following commutative diagram lifting the degenerate one in \(C\):

But then the morphism \(\xi \) lies in the fiber \(E_{pe''}\), which is an anima, so \(\xi \) is an isomorphism. In particular \(\xi \) is \(p\)-cocartesian, and hence so is \(\psi = \xi \circ \phi \).

Finally, assume that (3) holds, and consider a morphism \(\phi \colon e \to e'\) in \(E\) such that \(p\phi \) is invertible. We need to show that \(\phi \) is invertible. By assumption, there is an inverse \(g\colon pe' \to pe\) of \(p \phi \). We may then find a \(p\)-cocartesian lift \(\psi \colon e' \to e''\) of \(g\). But then \(\phi \circ \psi \) and \(\psi \circ \phi \) are cocartesian lifts of the respective identity maps on \(pe\) and \(pe'\). By uniqueness of cocartesian lifts (Lemma 23.1.7) these composites are isomorphisms. It follows that \(\phi \) is an isomorphism with inverse \(\psi \). □