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.15). 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.14, 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.13. 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.9. 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.15). 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.9). In particular, $v$ is $\lambda $-cocartesian (Proposition 5.1.1.9), so that $w = v \circ u$ is also $\lambda $-cocartesian (Proposition 5.1.4.13). $\square$

Proof of Proposition 8.2.1.8. The functor $\lambda _{-}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$ is a cocartesian fibration (Proposition 8.2.1.7) and is therefore exponentiable (Proposition 5.3.6.1). Let $\operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ and $\operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{C}}_{+} )$ be the relative exponentials introduced in Construction 4.5.9.1. Composition with $U$ induces a functor $V: \operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{C}}_{+} )$, which is an isofibration by virtue of Proposition 4.5.9.18. Let us identify the functor $\lambda _{+}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}_{+}$ with a section $s$ of the projection map $\operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{C}}_{+} ) \rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$, and form a pullback diagram

Since $V'$ is a pullback of $V$, it is also an isofibration (Remark 4.5.5.11). Moreover, the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+} }( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ can be identified with the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} }( \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{D}})$ of sections of $V'$.

For each object $X \in \operatorname{\mathcal{C}}_{-}$, let $\operatorname{\mathcal{C}}_{X}$ denote the fiber $\{ X\} \times _{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{C}}$. Unwinding the definitions, we can identify objects of $\operatorname{\mathcal{D}}$ with pairs $(X, F_ X)$, where $X$ is an object of $\operatorname{\mathcal{C}}_{-}$ and $F_ X: \operatorname{\mathcal{C}}_{X} \rightarrow \operatorname{\mathcal{E}}$ is a functor satisfying $U \circ f = \lambda _{+}|_{ \operatorname{\mathcal{C}}_{X} }$. For fixed $X \in \operatorname{\mathcal{C}}_{-}$, our assumption that $\lambda $ is corepresentable guarantees that the $\infty $-category $\operatorname{\mathcal{C}}_{X}$ has an initial object $C$. Set $Y = \lambda _{+}(C)$. By assumption, the $\infty $-category $\{ Y \} \times _{ \operatorname{\mathcal{C}}_{+} } \operatorname{\mathcal{E}}$ also has an initial object. Invoking the criterion of Corollary 7.3.6.11, we see that the $\infty $-category $\{ X\} \times _{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{D}}\simeq \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+} }( \operatorname{\mathcal{C}}_{X}, \operatorname{\mathcal{E}})$ also has an initial object. Moreover, an object $F_ X \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+} }( \operatorname{\mathcal{C}}_{X}, \operatorname{\mathcal{E}})$ is initial if and only if it satisfies the following pair of conditions:

$(1_{X})$

For every initial object $C \in \operatorname{\mathcal{C}}_{X}$, the image $F_ X(C)$ is an initial object of the $\infty $-category $\{ Y\} \times _{\operatorname{\mathcal{C}}_{+}} \operatorname{\mathcal{E}}$.

$(2_{X})$

The functor $F_ X$ carries each morphism in $\operatorname{\mathcal{C}}_{X}$ to a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$.

We will prove below that the functor $V'$ is a cartesian fibration. Assuming this Corollary 7.3.5.7, we guarantees that the $\infty $-category

has an initial object. Moreover, an object $F \in \operatorname{Fun}_{ / \operatorname{\mathcal{C}}_{+}}( \operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})$ is initial if and only if, for every object $X \in \operatorname{\mathcal{C}}_{-}$, the restriction $F_{X} = F|_{ \operatorname{\mathcal{C}}_{X} }$ satisfies conditions $(1_{X} )$ and $(2_{X} )$ above. Unwinding the definitions, this is equivalent to the requirement that $F$ satisfies condition $(1)$ and the following variant of condition $(2')$ of Remark 8.2.1.9:

$(2'')$

If $e$ is a morphism of $\operatorname{\mathcal{C}}$ such that $\lambda _{-}(e)$ is an identity morphism of $\operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$, then $F(e)$ is a $U$-cocartesian morphism of $\operatorname{\mathcal{E}}$.

The implication $(2') \Rightarrow (2'')$ is immediate. The reverse implication follows from the observation that if $\lambda _{-}(e)$ is an isomorphism in $\operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$, then $e$ is isomorphic (as an object of $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$) to a morphism $e'$ such that $\lambda _{-}(e')$ is an identity morphism of $\operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$.

We now complete the proof by showing that $V'$ is a cartesian fibration. Fix an object $(X, F_ X) \in \operatorname{\mathcal{D}}$, and a morphism $u: X' \rightarrow X$ in the $\infty $-category $\operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$. We wish to show that $u$ can be lifted to a $V'$-cartesian morphism $\widetilde{u}: (X', F_{X'}) \rightarrow (X, F_{X} )$ in the $\infty $-category $\operatorname{\mathcal{D}}$. We will prove a slightly stronger assertion: we can arrange that the image of $\widetilde{u}$ in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}/ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}, \operatorname{\mathcal{E}})$ is $V$-cartesian. Let us identify $u$ with a morphism $\Delta ^1 \rightarrow \operatorname{\mathcal{C}}_{-}^{\operatorname{op}}$ and set $\operatorname{\mathcal{C}}_{u} = \Delta ^1 \times _{ \operatorname{\mathcal{C}}_{-}^{\operatorname{op}} } \operatorname{\mathcal{C}}$, so that $\operatorname{\mathcal{C}}_{X}$ can be identified with the fiber $\{ 1\} \times _{ \Delta ^1} \operatorname{\mathcal{C}}_{u}$. By virtue of Corollary 7.3.7.6, it will suffice to show that the lifting problem

admits a solution having the property that $F_{u}$ is $U$-right Kan extended from $\operatorname{\mathcal{C}}_ X$.

Let $\pi : \operatorname{\mathcal{C}}_{u} \rightarrow \Delta ^1$ denote the projection map. Since $\pi $ is a pullback of $\lambda _{-}$, it is a cocartesian fibration of $\infty $-categories (Proposition 8.2.1.7). In particular, $\operatorname{\mathcal{C}}_{X}$ is a reflective subcategory of $\operatorname{\mathcal{C}}_{u}$. Moreover, if $C$ is an object of $\operatorname{\mathcal{C}}_{X}$, then a morphism $v: C' \rightarrow C$ in $\operatorname{\mathcal{C}}_{u}$ is $\pi $-cocartesian if and only if it exhibits $C$ as a $\operatorname{\mathcal{C}}_{X}$-reflection of $C'$ (see Proposition 6.2.2.24). By virtue of Corollary 7.3.5.9, it will suffice to show that if this condition is satisfied, then $\lambda _{+}(v)$ can be lifted to a $U$-cartesian morphism $E \rightarrow F_{X}(C)$ in $\operatorname{\mathcal{E}}$. This is clear: our assumption that $v$ is $\pi $-cocartesian guarantees that $\lambda _{+}(v)$ is an isomorphism in the $\infty $-category $\operatorname{\mathcal{C}}_{+}$ (Proposition 8.2.1.7), and can therefore be lifted to an isomorphism in $\operatorname{\mathcal{E}}$ by virtue of the fact that $U$ is an isofibration (Proposition 5.1.4.9). $\square$