Proposition 7.3.8.10. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ and $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be functors of $\infty $-categories, and suppose that $F$ is $U$-left Kan extended from a full subcategory $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$. Set $F_0 = F|_{ \operatorname{\mathcal{C}}^{0} }$. Then the restriction map
\[ \theta : \operatorname{\mathcal{D}}_{ F / } \rightarrow \operatorname{\mathcal{D}}_{ F_0 / } \times _{ \operatorname{\mathcal{E}}_{ (U \circ F_0) / } } \operatorname{\mathcal{E}}_{ (U \circ F) / } \]
is an equivalence of $\infty $-categories.
Proof.
Note that the restriction maps
\[ \operatorname{\mathcal{D}}_{F/} \rightarrow \operatorname{\mathcal{D}}_{F_0 / } \quad \quad \operatorname{\mathcal{D}}_{F_0 / } \rightarrow \operatorname{\mathcal{D}}\quad \quad \operatorname{\mathcal{E}}_{ (U \circ F) / } \rightarrow \operatorname{\mathcal{E}}_{ (U \circ F_0) / } \]
are left fibrations of simplicial sets (Corollary 4.3.6.12). It follows that we can regard $\theta $ as a functor of $\infty $-categories which are left-fibered over $\operatorname{\mathcal{D}}$. Consequently, to show that $\theta $ is an equivalence of $\infty $-categories, it will suffice to show that for every object $D \in \operatorname{\mathcal{D}}$, the commutative diagram
7.36
\begin{equation} \begin{gathered}\label{equation:coslice-over-Kan-extension} \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{D}}_{F/} \times _{\operatorname{\mathcal{D}}} \{ D\} \ar [r] \ar [d] & \operatorname{\mathcal{D}}_{F_0 /} \times _{\operatorname{\mathcal{D}}} \{ D\} \ar [d] \\ \operatorname{\mathcal{E}}_{ (U \circ F) / } \times _{\operatorname{\mathcal{E}}} \{ U(D) \} \ar [r] & \{ U(D) \} \times _{\operatorname{\mathcal{E}}_{ (U \circ F_0) / }} \times _{ \operatorname{\mathcal{E}}} \{ U(D) \} } \end{gathered} \end{equation}
induces a homotopy equivalence of Kan complexes
\[ \operatorname{\mathcal{D}}_{F/} \times _{\operatorname{\mathcal{D}}} \{ D\} \rightarrow (\operatorname{\mathcal{D}}_{ F_0 / } \times _{ \operatorname{\mathcal{E}}_{ (U \circ F_0) / } } \operatorname{\mathcal{E}}_{ (U \circ F) / }) \times _{\operatorname{\mathcal{D}}} \{ D \} . \]
Note that the horizontal maps in the diagram (7.36) are left fibrations between Kan complexes (Corollary 4.3.6.12), and therefore Kan fibrations (Corollary 4.4.3.8). We are therefore reduced to showing that the diagram (7.36) is a homotopy pullback square (Example 3.4.1.3).
Let $\underline{D} \in \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})$ denote the constant functor taking the value $D$. Using Theorem 4.6.4.17, we obtain a (termwise) homotopy equivalence from (7.36) to the diagram of morphism spaces
7.37
\begin{equation} \begin{gathered}\label{equation:coslice-over-Kan-extension2} \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}})}( F, \underline{D} ) \ar [r] \ar [d] & \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}^{0}, \operatorname{\mathcal{E}}) }( F_0, \underline{D}|_{ \operatorname{\mathcal{C}}^{0} } ) \ar [d] \\ \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}, \operatorname{\mathcal{E}})}( U \circ F, U \circ \underline{D} ) \ar [r] & \operatorname{Hom}_{ \operatorname{Fun}(\operatorname{\mathcal{C}}^{0}, \operatorname{\mathcal{E}})}( U \circ F_0, U \circ \underline{D}|_{ \operatorname{\mathcal{C}}^{0} } ). } \end{gathered} \end{equation}
Using Corollary 3.4.1.12, we are reduced to showing that the diagram (7.37) is a homotopy pullback square, which is a special case of Proposition 7.3.6.7.
$\square$