Kerodon

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

Corollary 5.1.4.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 5.1.3.5). If $f$ is a covariant equivalence relative to $S$, then $\theta $ is also a homotopy equivalence (Proposition 5.1.4.11), and therefore a trivial Kan fibration (Proposition 3.3.7.4). $\square$