$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Variant Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f: K \rightarrow \operatorname{\mathcal{C}}$ be a diagram, which we identify with an object $F$ of the $\infty $-category $\operatorname{Fun}(K, \operatorname{\mathcal{C}})$. Then the functors

\[ \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F} \quad \quad \operatorname{\mathcal{C}}_{f/} \rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{F/} \times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{\mathcal{C}} \]

of Exercise are equivalences of $\infty $-categories.

Proof. We will show that the slice diagonal $\delta _{/f}$ induces an equivalence of $\infty $-categories $\operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F}$; the analogous assertion for coslice $\infty $-categories follows by a similar argument. By virtue of Theorem, it will suffice to show that the inclusion map

\[ \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F} \hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ F \} \]

is an equivalence of $\infty $-categories. By construction, this map fits into a commutative diagram of $\infty $-categories

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}\times _{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F} \ar [r] \ar [d]^{\iota } & \operatorname{Fun}(K, \operatorname{\mathcal{C}})_{/F} \ar [d]^{U} \\ \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ F \} \ar [r] \ar [d] & \operatorname{Fun}(K, \operatorname{\mathcal{C}}) \operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) } \{ F \} \ar [d]^{V} \\ \operatorname{\mathcal{C}}\ar [r] & \operatorname{Fun}(K, \operatorname{\mathcal{C}}), } \]

where the upper square and lower square are both pullback diagrams. Note that the morphisms $V$ and $V \circ U$ are both right fibrations (Propositions and, and therefore isofibrations (Example Using Propositions and, we see that the upper square is a categorical pullback. Theorem guarantees that $U$ is an equivalence of $\infty $-categories, so that $\iota $ is an equivalence of $\infty $-categories by virtue of Proposition $\square$