Kerodon

Proof. Suppose first that $\lambda $ is a left fibration. Then $\lambda $ is a cocartesian fibration, and every morphism of $\operatorname{\mathcal{C}}$ is $\lambda $-cocartesian (Proposition 5.1.4.14). In particular, $\lambda $ is an isofibration. Let $\pi _{-}: \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}_{-}$ and $\pi _{+}: \operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+} \rightarrow \operatorname{\mathcal{C}}_{+}$ denote the projection maps. Note that $\pi _{-}$ is a cocartesian fibration, and that a morphism $(u_-, u_{+})$ of $\operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+}$ is $\pi _{-}$-cocartesian if and only if $u_{+} = \pi _{+}( u_{-}, u_{+} )$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_{+}$ (see Remark 5.1.4.6). Applying Proposition 5.1.4.13, we see that $\lambda _{-} = \pi _{-} \circ \lambda $ is also a cocartesian fibration, and that a morphism $u$ of $\operatorname{\mathcal{C}}$ is $\lambda _{-}$-cocartesian if and only if $\pi _{+}( \lambda (u) ) = \lambda _{+}(u)$ is an isomorphism in $\operatorname{\mathcal{C}}_{+}$. This proves assertion $(2)$, and assertion $(3)$ follows by a similar argument.

We now prove the converse. Suppose that $\lambda $ satisfies conditions $(1)$, $(2)$, and $(3)$; we wish to show that $\lambda $ is a left fibration. We first show that $\lambda $ is a cocartesian fibration. Fix an object $X \in \operatorname{\mathcal{C}}$ having image $\overline{X} = \lambda (X)$, together with a morphism $\overline{w}: \overline{X} \rightarrow \overline{Z}$ in the product $\operatorname{\mathcal{C}}_{-} \times \operatorname{\mathcal{C}}_{+}$. We wish to show that we can write $\overline{u} = \lambda (w)$ for some $\lambda $-cocartesian morphism $w: X \rightarrow Z$ in $\operatorname{\mathcal{C}}$. Invoking assumption $(2)$, we can choose a $\lambda _{-}$-cocartesian morphism $u: X \rightarrow Y$ of $\operatorname{\mathcal{C}}$ satisfying $\lambda _{-}(u) = \pi _{-}(\overline{w} )$. Set $\overline{Y} = \lambda (Y)$ and $\overline{u} = \lambda (u)$. Note that the morphism $\lambda _{+}(u) = \pi _{+}( \overline{u} )$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_{+}$. We can therefore choose a $2$-simplex $\overline{\sigma }$ of $\operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+}$ as indicated in the diagram

for which the image $\pi _{-}( \overline{\sigma } )$ is a right-degenerate $2$-simplex of $\operatorname{\mathcal{C}}^{\operatorname{op}}_{-}$. Note that, if $v$ can be lifted to a $\lambda $-cocartesian morphism $v: Y \rightarrow Z$ of $\operatorname{\mathcal{C}}$, then assumption $(1)$ guarantees that we can lift $\overline{\sigma }$ to a diagram

in the $\infty $-category $\operatorname{\mathcal{C}}$, where $w$ is $\lambda $-cocartesian by virtue of Proposition 5.1.4.12. Consequently, to prove the existence of $w$, we can replace $\overline{w}$ by $\overline{v}$ and thereby reduce to the case where $\lambda _{-}( \overline{w} )$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}^{\operatorname{op}}_{-}$. Repeating this argument with the roles of $\operatorname{\mathcal{C}}^{\operatorname{op}}_{-}$ and $\operatorname{\mathcal{C}}_{+}$ interchanged, we may also assume that $\lambda _{+}( \overline{w} )$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_{+}$. In this case, assumption $(1)$ guarantees that we can lift $\overline{w}$ to an isomorphism $w: X \rightarrow Z$ in the $\infty $-category $\operatorname{\mathcal{C}}$, which is $\lambda $-cocartesian by virtue of Proposition 5.1.1.8. This completes the proof that $\lambda $ is a cocartesian fibration.

To complete the proof that $\lambda $ is a left fibration, it will suffice to show that every morphism $w: X \rightarrow Z$ in $\operatorname{\mathcal{C}}$ is $\lambda $-cocartesian (see Proposition 5.1.4.14). Arguing as in Remark 5.1.3.8, we can choose a diagram

in $\operatorname{\mathcal{C}}$, where $u$ is $\lambda $-cocartesian and $\lambda (v)$ is an isomorphism in $\operatorname{\mathcal{C}}^{\operatorname{op}}_{-} \times \operatorname{\mathcal{C}}_{+}$. It follows from $(2)$ that $v$ is $\lambda _{-}$-cocartesian. Since $\lambda _{-}(v)$ is an isomorphism in $\operatorname{\mathcal{C}}^{\operatorname{op}}_{-}$, it follows that $v$ is an isomorphism in $\operatorname{\mathcal{C}}$ (Proposition 5.1.1.8). In particular, $v$ is $\lambda $-cocartesian (Proposition 5.1.1.8), so that $w = v \circ u$ is also $\lambda $-cocartesian (Proposition 5.1.4.12). $\square$