Kerodon

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

Example 5.5.2.23. Let $X$ be a Kan complex, and let $\operatorname{KFib}(X)$ denote the full subcategory of $\operatorname{Kan}_{/X}$ spanned by those morphisms $f: Y \rightarrow X$ which are Kan fibrations. If this condition is satisfied, then for every simplicial set $Z$, composition with $f$ induces a Kan fibration $\operatorname{Fun}(Z, Y) \rightarrow \operatorname{Fun}(Z, X)$ (Corollary 3.1.3.2). Applying (the dual of) Proposition 5.5.2.22, we obtain a fully faithful functor of $\infty $-categories

\[ \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{KFib}(X) ) \rightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{Kan})_{/X} = \operatorname{\mathcal{S}}_{/X}. \]

In fact, this functor is an equivalence of $\infty $-categories: its essential surjectivity follows from the observation that an arbitrary morphism of Kan complexes $f: Y \rightarrow X$ admits a factorization $Y \xrightarrow {e} Y' \xrightarrow {f'} X$, where $f'$ is a Kan fibration and $e$ is a homotopy equivalence (Proposition 3.1.7.1).