Proof.
We first show that $(1)$ implies $(2)$. Let $F: A \rightarrow B$ be a left cofinal morphism of simplicial sets; we wish to show that the diagram (7.10) is a categorical pushout square. By virtue of Corollary 7.2.1.15 (and Proposition 4.5.4.8), we may assume that $F$ is either left anodyne or a trivial Kan fibration. In the second case, the vertical morphisms in the diagram (7.10) are categorical equivalences (see Corollary 4.5.8.9), so the desired result is a special case of Proposition 4.5.4.10. In the second case, Example 4.3.6.5 guarantees that the induced map $B \coprod _{A} A^{\triangleleft } \hookrightarrow B^{\triangleleft }$ is inner anodyne, so the desired result follows from Proposition 4.5.4.11.
Notation 4.5.8.3 supplies a comparison map from the diagram (7.11) to the diagram (7.10), whcih is a levelwise categorical equivalence by virtue of Theorem 4.5.8.8. The equivalence $(2) \Leftrightarrow (3)$ now follows from Proposition 4.5.4.9.
We next show that $(3)$ implies $(4)$. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $G: B \rightarrow \operatorname{\mathcal{C}}$ be a diagram. If condition $(3)$ is satisfied, then the diagram of $\infty $-categories
\[ \xymatrix { \operatorname{Fun}( \Delta ^0 \diamond B, \operatorname{\mathcal{C}}) \ar [r] \ar [d] & \operatorname{Fun}( \Delta ^0 \diamond A, \operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{Fun}( B, \operatorname{\mathcal{C}}) \ar [r]^{ \circ F} & \operatorname{Fun}(A, \operatorname{\mathcal{C}}) } \]
is a categorical pullback square. Corollary 4.4.5.3 guaranteees that the vertical maps in this diagram are isofibrations. Invoking Corollary 4.5.2.31 (together with the definition of the blunt join), we deduce that the induced map
\begin{eqnarray*} \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(B, \operatorname{\mathcal{C}}) } \{ G\} & \simeq & \operatorname{Fun}( \Delta ^0 \diamond B, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(B, \operatorname{\mathcal{C}}) } \{ G\} \\ & \rightarrow & \operatorname{Fun}( \Delta ^0 \diamond A, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(A, \operatorname{\mathcal{C}}) } \{ G \circ F\} \\ & \simeq & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}( A, \operatorname{\mathcal{C}}) } \{ G \circ F\} \end{eqnarray*}
is an equivalence of $\infty $-categories.
We next prove the equivalences $(4) \Leftrightarrow (5) \Leftrightarrow (6) \Leftrightarrow (7)$. Let $G: B \rightarrow \operatorname{\mathcal{C}}$ be as above. Applying Construction 4.6.4.13, we obtain a commutative diagram of $\infty $-categories
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{/G} \ar [r] \ar [d]^{\theta } & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(B, \operatorname{\mathcal{C}}) } \{ G\} \ar [d]^{\theta '} \\ \operatorname{\mathcal{C}}_{ / (G \circ F)} \ar [r] & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(A, \operatorname{\mathcal{C}}) } \{ G \circ F \} , } \]
where the horizontal maps are equivalences of $\infty $-categories (Theorem 4.6.4.17). It follows that $\theta $ is an equivalence of $\infty $-categories if and only if $\theta '$ is an equivalence of $\infty $-categories. This proves the equivalence $(4) \Leftrightarrow (5)$. Note that the functor $\theta '$ fits into a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(B, \operatorname{\mathcal{C}}) } \{ G\} \ar [dr] \ar [rr]^{\theta '} & & \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(A, \operatorname{\mathcal{C}}) } \{ G \circ F \} \ar [dl] \\ & \operatorname{\mathcal{C}}, & } \]
where the vertical maps are right fibrations (Corollary 4.6.4.12). Applying Corollary 5.1.7.16 and Proposition 5.1.7.5, we see that $\theta '$ is an equivalence of $\infty $-categories if and only if it induces a homotopy equivalence
\[ \theta '_{X}: \{ \underline{X} \} \operatorname{\vec{\times }}_{ \operatorname{Fun}(B, \operatorname{\mathcal{C}}) } \{ G\} \rightarrow \{ \underline{X} \circ F \} \operatorname{\vec{\times }}_{ \operatorname{Fun}(A, \operatorname{\mathcal{C}}) } \{ G \circ F \} \]
for each object $X \in \operatorname{\mathcal{C}}$, which proves the equivalence $(4) \Leftrightarrow (6)$. Unwinding the definitions, we can identify $\theta '$ with the lower horizontal map appearing in the diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( B, \operatorname{\mathcal{C}}_{X/} ) \ar [r]^-{\theta ''_{X}} \ar [d] & \operatorname{Fun}_{ / \operatorname{\mathcal{C}}}( A, \operatorname{\mathcal{C}}_{X/} ) \ar [d] \\ \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( B, \{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}) \ar [r]^-{\theta '_{X}} & \operatorname{Fun}_{/\operatorname{\mathcal{C}}}( A, \{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}), } \]
where the vertical maps are given by postcomposition with the coslice diagonal morphism $\rho : \operatorname{\mathcal{C}}_{X/} \rightarrow \{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}$. Theorem 4.6.4.17 guarantees that $\rho $ is an equivalence of $\infty $-categories. It is therefore also an an equivalence of left fibrations over $\operatorname{\mathcal{C}}$ (Proposition 5.1.7.5), so that the vertical maps are homotopy equivalences. It follows that $\theta '_{X}$ is a homotopy equivalence if and only if $\theta ''_{X}$ is a homotopy equivalence, which proves the equivalence $(6) \Leftrightarrow (7)$.
We now complete the proof by showing that $(7)$ implies $(1)$. Assume that condition $(7)$ is satisfied; we wish to show that $F$ is left cofinal. Let $q: \widetilde{B} \rightarrow B$ be a left fibration; we must show that composition with $F$ induces a homotopy equivalence $\operatorname{Fun}_{/B}( B, \widetilde{B} ) \rightarrow \operatorname{Fun}_{/B}(A, \widetilde{B} )$. To prove this, we are free to replace $q: \widetilde{B} \rightarrow B$ by any other left fibration which is equivalent to it (in the sense of Definition 5.1.7.1). We may therefore assume without loss of generality that there exists a pullback diagram of simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \widetilde{B} \ar [r] \ar [d]^{q} & \operatorname{\mathcal{S}}_{\ast } \ar [d]^{q_{\mathrm{univ}}} \\ B \ar [r]^-{G} & \operatorname{\mathcal{S}}, } \]
where $q_{\mathrm{univ}}: \operatorname{\mathcal{S}}_{\ast } \rightarrow \operatorname{\mathcal{S}}$ is the universal left fibration of Corollary 5.6.0.6. We are then reduced to proving that $F$ induces a homotopy equivalence $\operatorname{Fun}_{ / \operatorname{\mathcal{S}}}( B, \operatorname{\mathcal{S}}_{\ast } ) \rightarrow \operatorname{Fun}_{ \operatorname{\mathcal{S}}}( A, \operatorname{\mathcal{S}}_{\ast } )$, which is a special case of $(7)$ (applied to the $\infty $-category $\operatorname{\mathcal{C}}= \operatorname{\mathcal{S}}$ and the object $X = \Delta ^0$).
$\square$