Proposition 7.1.5.12. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty $-categories and let $\overline{f}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$. Then $\overline{f}$ is a $U$-limit diagram if and only if, for every object $C \in \operatorname{\mathcal{C}}$, the diagram of morphism spaces
7.1
\begin{equation} \begin{gathered}\label{equation:U-colimit-by-morphism-space} \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}}) }( \underline{C}, \overline{f} ) \ar [r] \ar [d] & \operatorname{Hom}_{\operatorname{Fun}(K, \operatorname{\mathcal{C}}) }( \underline{C}|_{K}, \overline{f}|_{K} ) \ar [d] \\ \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{D}}) }( U \circ \underline{C}, U \circ \overline{f} ) \ar [r] & \operatorname{Hom}_{\operatorname{Fun}(K, \operatorname{\mathcal{D}}) }( U \circ \underline{C}|_{K}, U \circ \overline{f}|_{K} ) } \end{gathered} \end{equation}
is a homotopy pullback square; here we let $\underline{C} \in \operatorname{Fun}( K^{\triangleleft }, \operatorname{\mathcal{C}})$ denote the constant diagram taking the value $C$.
Proof.
Set $f = \overline{f}|_{K}$. Note that the restriction maps
\[ \operatorname{\mathcal{C}}_{/\overline{f}} \rightarrow \operatorname{\mathcal{C}}_{/f } \quad \quad \operatorname{\mathcal{C}}_{/f} \rightarrow \operatorname{\mathcal{C}}\quad \quad \operatorname{\mathcal{D}}_{ / (U \circ \overline{f} )} \rightarrow \operatorname{\mathcal{D}}_{/(U \circ f) } \]
are right fibrations of simplicial sets (Corollary 4.3.6.11). It follows that we can regard the map
\[ U': \operatorname{\mathcal{C}}_{ / \overline{f} } \rightarrow \operatorname{\mathcal{C}}_{/f} \times _{ \operatorname{\mathcal{D}}_{/(U \circ f)}} \operatorname{\mathcal{D}}_{ / (U \circ \overline{f} ) } \]
of Remark 7.1.5.8 as a functor between $\infty $-categories which are right-fibered over $\operatorname{\mathcal{C}}$. Combining Remark 7.1.5.8 with the criterion of Corollary 5.1.6.4, we see that $\overline{f}$ is a $U$-colimit diagram if and only if, for every object $C \in \operatorname{\mathcal{C}}$, the induced map
\[ U'_{C}: \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{ / \overline{f} } \rightarrow \{ C\} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/f} \times _{ \operatorname{\mathcal{D}}_{/(U \circ f)}} \operatorname{\mathcal{D}}_{ / (U \circ \overline{f} ) } \]
is a homotopy equivalence of Kan complexes.
To complete the proof, it will suffice to show that $U'_{C}$ is a homotopy equivalence if and only if the diagram (7.1) is a homotopy pullback square. To see this, we note that Proposition 4.6.5.10 supplies a levelwise homotopy equivalence of (7.1) with the diagram
7.2
\begin{equation} \begin{gathered}\label{equation:U-colimit-by-morphism-space2} \xymatrix@R =50pt@C=50pt{ \{ C\} \times _{ \operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{ / \overline{f} } \ar [r] \ar [d] & \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}_{/f} \ar [d] \\ \{ U(C) \} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{ / (U \circ \overline{f} )} \ar [r] & \{ U(C) \} \times _{\operatorname{\mathcal{D}}} \operatorname{\mathcal{D}}_{ / (U \circ f) }. } \end{gathered} \end{equation}
It will therefore suffice to show that (7.2) is a homotopy pullback square if and only if $U'_{C}$ is a homotopy equivalence (Corollary 3.4.1.12). This is a special case of Example 3.4.1.3, since the horizontal maps in the diagram (7.2) are Kan fibrations (combine Corollaries 4.3.6.11 and 4.4.3.8).
$\square$