Kerodon

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

Corollary 9.3.1.20. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ and $F: K \rightarrow \operatorname{\mathcal{E}}$ be morphisms of simplicial sets and let $n$ be an integer. Assume that $U$ is a right fibration with $n$-truncated fibers and that $K$ is $(n+1)$-connective. Then the map $U_{ /F}: \operatorname{\mathcal{E}}_{/F} \rightarrow \operatorname{\mathcal{C}}_{ / \overline{F} }$ is a trivial Kan fibration.