Proof.
Without loss of generality, we may assume that $\operatorname{\mathcal{C}}$ is an $\infty $-category (working one simplex at a time, we could even assume that $\operatorname{\mathcal{C}}= \Delta ^ m$ is a standard simplex and that $\operatorname{\mathcal{C}}_0 = \operatorname{\partial \Delta }^ m$ is its boundary). Set $\overline{\operatorname{\mathcal{K}}} = \operatorname{\mathcal{K}}\star _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}$, so that $\delta $ extends to a map
\[ \overline{\delta }: \overline{\operatorname{\mathcal{K}}} = \operatorname{\mathcal{K}}\star _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\star _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\simeq \Delta ^1 \times \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}. \]
Since $\delta $ is a cocartesian fibration, Lemma 5.2.3.17 guarantees that $\overline{\delta }$ is also a cocartesian fibration. Applying Corollary 5.3.6.8, we obtain a commutative diagram of $\infty $-categories
7.16
\begin{equation} \begin{gathered}\label{equation:diagram-of-Res} \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \ar [rr] \ar [dd]^{U \circ } \ar [dr]^{T} & & \operatorname{Fun}( \operatorname{\mathcal{K}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \ar [dd]^{U \circ } \ar [dl] \\ & \operatorname{\mathcal{C}}& \\ \operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \ar [rr] \ar [ur] & & \operatorname{Fun}( \operatorname{\mathcal{K}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}), \ar [ul] } \end{gathered} \end{equation}
where the diagonal arrows are cartesian fibrations and the morphisms on the outside of the diagram preserve cartesian morphisms. Applying Proposition 5.1.4.21, we see that the induced map
\[ T': \operatorname{Fun}(\operatorname{\mathcal{K}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})) \times _{ \operatorname{Fun}( \operatorname{\mathcal{K}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) } \operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}} \]
is also a cartesian fibration, and that the outer square of the diagram (7.16) determines a functor
\[ V: \operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}(\operatorname{\mathcal{K}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})) \times _{ \operatorname{Fun}( \operatorname{\mathcal{K}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) } \operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) \rightarrow \operatorname{\mathcal{C}} \]
which carries $T$-cartesian morphisms to $T'$-cartesian morphisms.
We next claim that $V$ is an isofibration. Fix a monomorphism of simplicial sets $i: A \hookrightarrow B$ which is also a categorical equivalence; we wish to show that every diagram
\[ \xymatrix@C =50pt@R=50pt{ A \ar [r] \ar [d] & \operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \ar [d]^{V} \\ B \ar [r] \ar@ {-->}[ur] & \operatorname{Fun}(\operatorname{\mathcal{K}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})) \times _{ \operatorname{Fun}( \operatorname{\mathcal{K}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) } \operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) } \]
admits a solution. Note that this lifting problem determines a morphism of simplicial sets $B \rightarrow \operatorname{\mathcal{C}}$. Invoking the universal property of Proposition 4.5.9.5, we can rewrite this as a lifting problem
\[ \xymatrix@C =50pt@R=50pt{ (A \times _{\operatorname{\mathcal{C}}} \overline{\operatorname{\mathcal{K}}}) {\coprod }_{(A \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{K}}) } (B \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{K}}) \ar [r] \ar [d] & \operatorname{\mathcal{D}}\ar [d]^{U} \\ B \times _{\operatorname{\mathcal{C}}} \overline{\operatorname{\mathcal{K}}} \ar@ {-->}[ur] \ar [r] & \operatorname{\mathcal{E}}. } \]
Since $U$ is an isofibration, it will suffice to show that the left vertical map is a categorical equivalence of simplicial sets, or equivalently that the diagram
\[ \xymatrix@C =50pt@R=50pt{ A \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{K}}\ar [r] \ar [d] & B \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{K}}\ar [d] \\ A \times _{\operatorname{\mathcal{C}}} \overline{\operatorname{\mathcal{K}}} \ar [r] & B \times _{\operatorname{\mathcal{C}}} \overline{\operatorname{\mathcal{K}}} } \]
is a categorical pushout square (Proposition 4.5.4.11). This follows from Proposition 4.5.4.10, since the horizontal maps are categorical equivalences (Corollary 5.6.7.6).
Unwinding the definitions, we can rewrite (7.15) as a lifting problem
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_0 \ar [r]^-{ G_0} \ar [d] & \operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \ar [d]^{V} & \\ \operatorname{\mathcal{C}}\ar [r] \ar@ {-->}[ur] & \operatorname{Fun}(\operatorname{\mathcal{K}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})) \times _{ \operatorname{Fun}( \operatorname{\mathcal{K}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) } \operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}}) . } \]
By virtue of Corollary 7.1.7.9, to show that this lifting problem admits a solution, it will suffice to verify the following:
- $(\ast ')$
Let $\sigma : \Delta ^ n \rightarrow \operatorname{\mathcal{C}}$ be an $n$-simplex which is not contained in $\operatorname{\mathcal{C}}_0$ and set $C = \sigma (0)$. Then $G_0(C)$ is a $V$-initial object of the $\infty $-category $\operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$.
Unwinding the definitions, we see that the functor $T^{-1} \{ C\} \rightarrow T'^{-1} \{ C\} $ induced by $V$ can be identified with the restriction map
\[ V_ C: \operatorname{Fun}( \operatorname{\mathcal{K}}_{C}^{\triangleright }, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{K}}_ C, \operatorname{\mathcal{D}}) \times _{ \operatorname{Fun}( \operatorname{\mathcal{K}}_ C, \operatorname{\mathcal{E}}) } \operatorname{Fun}( \operatorname{\mathcal{K}}_ C^{\triangleright }, \operatorname{\mathcal{E}}). \]
Combining assumption $(\ast )$ with Proposition 7.1.7.4, we see that $G_0( C )$ is a $V_ C$-initial object of the $\infty $-category $\operatorname{Fun}( K_{C}^{\triangleright }, \operatorname{\mathcal{D}})$. Proposition 7.1.5.19 then guarantees that $G_0(C)$ is also $V$-initial when regarded as an object of the $\infty $-category $\operatorname{Fun}( \overline{\operatorname{\mathcal{K}}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$.
$\square$