Theorem 4.6.4.17. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $F: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram. Then the slice and coslice diagonal maps
\[ \delta _{/F}: \operatorname{\mathcal{C}}_{/F} \hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ F\} \quad \quad \delta _{F/}: \operatorname{\mathcal{C}}_{F/} \hookrightarrow \{ F\} \operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}} \]
are equivalences of $\infty $-categories.
Proof of Theorem 4.6.4.17.
Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $F: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram, which we regard as an object of the $\infty $-category $\operatorname{Fun}(K,\operatorname{\mathcal{C}})$. We will show that the slice diagonal morphism
\[ \delta _{/F}: \operatorname{\mathcal{C}}_{/F} \hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ F\} \]
is an equivalence of $\infty $-categories; the corresponding assertion for the coslice diagonal morphism follows by a similar argument. Fix a simplicial set $J$; we wish to show that the induced map of sets
\[ \theta : \pi _0( \operatorname{Fun}(J, \operatorname{\mathcal{C}}_{/F} )^{\simeq } ) \rightarrow \pi _0( \operatorname{Fun}( J, \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K,\operatorname{\mathcal{C}})} \{ F\} )^{\simeq } ) \]
is a bijection. Using Lemma 4.6.4.22, Variant 4.6.4.23, and Remark 4.6.4.14, we can identify $\theta $ with the map of sets
\[ \pi _0( \operatorname{Fun}_{K/}( J \star K, \operatorname{\mathcal{C}})^{\simeq } ) \rightarrow \pi _0( \operatorname{Fun}_{K/}( J \diamond K, \operatorname{\mathcal{C}})^{\simeq } ) \]
induced by precomposition with the comparison map $c_{J,K}: J \diamond K \twoheadrightarrow J \star K$ of Notation 4.5.8.3. It will therefore suffice to show that composition with $c_{J,K}$ induces an equivalence of $\infty $-categories $\operatorname{Fun}_{K/}( J \star K, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}_{K/}( J \diamond K, \operatorname{\mathcal{C}})$. This follows by applying Corollary 4.5.2.26 to the commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}( J \star K, \operatorname{\mathcal{C}}) \ar [r]^-{\circ c_{J,K}} \ar [d] & \operatorname{Fun}( J \diamond K, \operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{Fun}( K, \operatorname{\mathcal{C}}) \ar@ {=}[r] & \operatorname{Fun}( K, \operatorname{\mathcal{C}}); } \]
here the vertical maps are isofibrations (Corollary 4.4.5.3) and the upper horizontal map is an equivalence of $\infty $-categories because the morphism $c_{J,K}$ is a categorical equivalence (Theorem 4.5.8.8).
$\square$