# Kerodon

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

Proposition 4.6.8.4. Let $q: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be an inner fibration of simplicial sets, and let $X_0, X_1, \ldots , X_ n$ be vertices of $\operatorname{\mathcal{C}}$ having images $\overline{X}_0, \overline{X}_1, \ldots , \overline{X}_ n \in \operatorname{\mathcal{D}}$. Then the restriction map

$\xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X_0, \cdots , X_ n) \ar [d]^{\theta } \\ \operatorname{Hom}_{\operatorname{\mathcal{D}}}( \overline{X}_0, \cdots , \overline{X}_ n) \times _{ \prod _{i=1}^{n} \operatorname{Hom}_{\operatorname{\mathcal{D}}}( \overline{X}_{i-1}, \overline{X}_{i})} \prod _{i=1}^{n} \operatorname{Hom}_{\operatorname{\mathcal{C}}}( X_{i-1}, X_{i} ) }$

is a trivial Kan fibration of simplicial sets.

Proof. Let $\operatorname{Spine}[n]$ denote the spine of the standard $n$-simplex $\Delta ^ n$ (see Example 1.4.7.7). Unwinding the definitions, we see that $\theta$ is a pullback of the restriction map

$\theta ': \operatorname{Fun}( \Delta ^ n, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \operatorname{Spine}[n], \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}( \operatorname{Spine}[n], \operatorname{\mathcal{D}}) } \operatorname{Fun}( \Delta ^ n, \operatorname{\mathcal{D}}).$

Since $q$ is an inner fibration and the inclusion $\operatorname{Spine}[n] \hookrightarrow \Delta ^ n$ is inner anodyne (Example 1.4.7.7), the morphism $\theta '$ is a trivial Kan fibration (Proposition 4.1.4.4). $\square$