Proof.
Let $v$ denote the cone point of $\operatorname{\mathcal{C}}^{\triangleright } = \operatorname{\mathcal{C}}\star \{ v\} $ and let $\overline{\operatorname{\mathcal{E}}}_{v} = \{ v\} \times _{\operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}$ denote the corresponding fiber of $\overline{\operatorname{\mathcal{E}}}$. Since the inclusion map $\{ v \} \hookrightarrow \operatorname{\mathcal{C}}^{\triangleright }$ is right anodyne (Example 4.3.7.11), the inclusion $\iota : \overline{\operatorname{\mathcal{E}}}_{ v } \hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is also right anodyne (Corollary 7.2.3.13). In particular, $\iota $ is a weak homotopy equivalence of simplicial sets.
Let $q: \Delta ^1 \times \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}^{\triangleright }$ be the morphism of simplicial sets characterized by the requirement that $q|_{ \{ 0\} \times \operatorname{\mathcal{C}}^{\triangleright } }$ is the identity morphism and $q|_{ \{ 1\} \times \operatorname{\mathcal{C}}^{\triangleright } }$ is the constant morphism taking the value $v$. Set $X = \overline{\mathscr {F}}(v)$, so that the composition
\[ \Delta ^1 \times \operatorname{\mathcal{C}}^{\triangleright } \xrightarrow {q} \operatorname{\mathcal{C}}^{\triangleright } \xrightarrow { \overline{\mathscr {F}} } \operatorname{\mathcal{S}}^{< \kappa } \]
can be identified with a natural transformation $\beta : \overline{\mathscr {F}} \rightarrow \underline{X}|_{\operatorname{\mathcal{C}}^{\triangleright }}$.
Choose a natural transformation $\alpha : \underline{ \Delta ^{0} }_{ \overline{\operatorname{\mathcal{E}}} } \rightarrow \overline{\mathscr {F}}|_{ \overline{\operatorname{\mathcal{E}}} }$ which exhibits $\overline{\mathscr {F}}$ as a covariant transport representation for $\overline{U}$, and let $\gamma : \underline{ \Delta ^{0} }|_{ \overline{\operatorname{\mathcal{E}}} } \rightarrow \underline{X}_{ \overline{\operatorname{\mathcal{E}}} }$ be a composition of $\beta |_{ \overline{\operatorname{\mathcal{E}}} }$ with $\alpha $. Then $\gamma $ can be identified with a morphism of simplicial sets $T: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{S}}^{< \kappa } }( \Delta ^0, X)$. Our assumption on $\alpha $ guarantees that the the composite map
\[ \overline{\operatorname{\mathcal{E}}}_{v} \xrightarrow {\iota } \overline{\operatorname{\mathcal{E}}} \xrightarrow {T} X \]
is a weak homotopy equivalence of simplicial sets. We can therefore reformulate condition $(1)$ as follows:
- $(1')$
The restriction $T|_{\operatorname{\mathcal{E}}}: \operatorname{\mathcal{E}}\rightarrow \operatorname{Hom}_{\operatorname{\mathcal{S}}^{< \kappa } }( \Delta ^0, X)$ is a weak homotopy equivalence.
Set $\mathscr {F} = \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}}$. Using Proposition 7.4.3.13, we see that $(1')$ is equivalent to the requirement that the natural transformation $\beta |_{\operatorname{\mathcal{C}}}: \mathscr {F} \rightarrow \underline{X}_{\operatorname{\mathcal{C}}}$ exhibits $X$ as a colimit of $\mathscr {F}$. The equivalence $(1') \Leftrightarrow (3)$ now follows from Remark 7.1.3.6.
The implication $(2) \Rightarrow (1)$ follows from Proposition 7.2.1.5. We will complete the proof by showing that $(1)$ implies $(2)$. monomorphism $\operatorname{\mathcal{C}}\hookrightarrow \operatorname{\mathcal{C}}'$, where $\operatorname{\mathcal{C}}'$ is an $\infty $-category. Then the induced map $\operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$ is also inner anodyne (Corollary 4.3.6.6); in particular, it is a categorical equivalence. Using Proposition 5.6.7.2 (and Remark 5.6.7.4), we can assume that $\overline{U}$ is the pullback of a left fibration $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$. Setting $\operatorname{\mathcal{E}}' = \operatorname{\mathcal{C}}' \times _{ \operatorname{\mathcal{C}}'^{\triangleright } } \overline{\operatorname{\mathcal{E}}}'$, we have a commutative diagram of inclusion maps
\[ \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}\ar [r] \ar [d] & \overline{\operatorname{\mathcal{E}}} \ar [d] \\ \operatorname{\mathcal{E}}' \ar [r] & \overline{\operatorname{\mathcal{E}}'}, } \]
where the vertical maps are categorical equivalences (Corollary 5.6.7.6). Consequently, to prove that the inclusion map $\operatorname{\mathcal{E}}\hookrightarrow \overline{\operatorname{\mathcal{E}}}$ is left cofinal, it will suffice to show that the inclusion $\operatorname{\mathcal{E}}' \hookrightarrow \overline{\operatorname{\mathcal{E}}}'$ is left cofinal (Corollary 7.2.1.22). We may therefore replace $\overline{U}$ by the left fibration $\overline{U}': \overline{\operatorname{\mathcal{E}}}' \rightarrow \operatorname{\mathcal{C}}'^{\triangleright }$, and thereby reduce to proving the implication $(1) \Rightarrow (2)$ under the assumption that $\operatorname{\mathcal{C}}$ is an $\infty $-category.
Let $\operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \overline{\operatorname{\mathcal{E}}}_{v}$ denote the oriented fiber product of Definition 4.6.4.1, so that the diagram of simplicial sets
\[ \xymatrix { \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \overline{\operatorname{\mathcal{E}}}_{v} \ar [r]^{ \pi } \ar [r]^{ \pi ' } & \overline{\operatorname{\mathcal{E}}}_{v} \ar [d]^{\iota } \\ \operatorname{\mathcal{E}}\ar [r] & \overline{\operatorname{\mathcal{E}}} } \]
commutes up to homotopy. Assume that condition $(1)$ is satisfied: that is, the lower horizontal map is a weak homotopy equivalence. Since $\pi $ is a trivial Kan fibration and $\iota $ is a weak homotopy equivalence, it follows that $\pi '$ is also a weak homotopy equivalence. For each vertex $X \in \overline{\operatorname{\mathcal{E}}}_{v}$, we have a pullback diagram of simplicial sets
7.51
\begin{equation} \begin{gathered}\label{equation:diagram-for-left-cofinality} \xymatrix@C =50pt@R=50pt{ \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \{ X \} \ar [r] \ar [d] & \{ X\} \ar [d] \\ \operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \overline{\operatorname{\mathcal{E}}}_{v} \ar [r]^-{ \pi ' } & \overline{\operatorname{\mathcal{E}}}_{v}. } \end{gathered} \end{equation}
Since $\pi '$ is an isofibration of $\infty $-categories (Corollary 5.3.7.3), the diagram( 7.51) is a categorical pullback square (Corollary 4.5.2.27). Because $\overline{\operatorname{\mathcal{E}}}_{v}$ is a Kan complex, the diagram (7.51) is also a homotopy pullback square (Variant 4.5.2.11). Since $\pi '$ is a weak homotopy equivalence, it follows that the upper horizontal map is also a weak homotopy equivalence: that is, the oriented fiber product $\operatorname{\mathcal{E}}\operatorname{\vec{\times }}_{ \overline{\operatorname{\mathcal{E}}} } \{ X\} $ is weakly contractible (Corollary 3.4.1.5). Condition $(2)$ now follows by allowing the object $X$ to vary and applying the criterion of of Theorem 7.2.3.1 (together with Remark 7.2.3.2).
$\square$