Kerodon

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

Remark 7.1.6.13. We will see later that, if $\overline{f}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ is a $U$-limit diagram, then it satisfies a stronger version of the criterion of Proposition 7.1.7.5: for every morphism $\overline{g}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$, the diagram of Kan complexes

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}}) }( \overline{g}, \overline{f} ) \ar [r] \ar [d] & \operatorname{Hom}_{\operatorname{Fun}(K, \operatorname{\mathcal{C}}) }( \overline{g}|_{K}, \overline{f}|_{K} ) \ar [d] \\ \operatorname{Hom}_{\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{D}}) }( U \circ \overline{g}, U \circ \overline{f} ) \ar [r] & \operatorname{Hom}_{\operatorname{Fun}(K, \operatorname{\mathcal{D}}) }( U \circ \overline{g}|_{K}, U \circ \overline{f}|_{K} ) } \]

is a homotopy pullback square. See Remark 7.1.7.5.