Lemma 9.2.8.4. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category containing morphisms $f: A \rightarrow B$ and $g: X \rightarrow Y$. Then precomposition with the inclusion map $\operatorname{N}_{\bullet }( \{ 1 < 2 \} ) \hookrightarrow \Delta ^3$ induces a trivial Kan fibration of simplicial sets ${}_{f}\operatorname{Fun}(\Delta ^3, \operatorname{\mathcal{C}})_{g} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}( B, X )$. In particular, the simplicial set ${}_{f}\operatorname{Fun}(\Delta ^3, \operatorname{\mathcal{C}})_{g}$ is a Kan complex.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. By construction, we have a pullback diagram of simplicial sets
\[ \xymatrix@R =50pt@C=50pt{ \empty {}_{f}\operatorname{Fun}(\Delta ^3, \operatorname{\mathcal{C}})_{g} \ar [d] \ar [r] & \operatorname{Fun}( \Delta ^3, \operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(B,X) \ar [r] & \operatorname{Fun}( \operatorname{Spine}[3], \operatorname{\mathcal{C}}), } \]
where the right vertical map is a trivial Kan fibration (see Example 1.5.7.7). $\square$