# Kerodon

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

Remark 5.7.7.4. In the situation of Corollary 5.7.7.3, if $U_0$ is a left fibration, then $U$ is also a left fibration. To see this, it suffices to show that the fibers of $U$ are Kan complexes (Proposition 5.1.4.14). This is clear, since every fiber of $U$ is also a fiber of $U_0$ (note that the inner anodyne morphism $F: \operatorname{\mathcal{C}}_0 \rightarrow \operatorname{\mathcal{C}}$ is bijective at the level of vertices; see Exercise 1.4.6.6).