# Kerodon

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

Corollary 8.9.8.12. Suppose we are given a commutative diagram of simplicial sets

$\xymatrix@R =50pt@C=50pt{ X \ar [rr]^{f} \ar [dr] & & Y \ar [dl] \\ & S, & }$

where $f$ is a monomorphism. If $q: Z \rightarrow S$ is a left fibration of simplicial sets and $f$ is a covariant equivalence relative to $S$, then the induced map $\theta : \operatorname{Fun}_{/S}(Y,Z) \rightarrow \operatorname{Fun}_{/S}(X,Z)$ is a trivial Kan fibration. Similarly, if $q: Z \rightarrow S$ is a right fibration and $f$ is a contravariant equivalence relative to $S$, then $\theta$ is a trivial Kan fibration.

Proof. We will prove the first assertion; the proof of the second is similar. If $q$ is a left fibration, then the morphism $\theta : \operatorname{Fun}_{/S}(Y,Z) \rightarrow \operatorname{Fun}_{/S}(X,Z)$ is a Kan fibration (Proposition 8.9.7.5). If $f$ is a covariant equivalence relative to $S$, then $\theta$ is also a homotopy equivalence (Proposition 8.9.8.11), and therefore a trivial Kan fibration (Proposition 3.3.7.4). $\square$