# Kerodon

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

Corollary 4.3.7.3. Let $f: K \rightarrow X$ and $q: X \rightarrow S$ be morphisms of simplicial sets. Then:

• If $q$ is a left fibration, then the induced map

$X_{/f} \rightarrow X \times _{ S} S_{/ (q \circ f)}$

is a Kan fibration.

• If $q$ is a right fibration, then the induced map

$X_{f/} \rightarrow X \times _{ S} S_{(q \circ f)/}$

is a Kan fibration.

Proof. Apply Proposition 4.3.7.2 in the special case $K_0 = \emptyset$. $\square$