# Kerodon

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

Proposition 4.5.5.18. Let $q: X \rightarrow S$ be an isofibration of simplicial sets and let $i: A \hookrightarrow B$ be a monomorphism of simplicial sets. If $i$ is a categorical equivalence, then the restriction map

$q': \operatorname{Fun}(B,X) \rightarrow \operatorname{Fun}(A,X) \times _{ \operatorname{Fun}(A,S) } \operatorname{Fun}(B,S)$

is a trivial Kan fibration.

Proof. Let $B'$ be a simplicial set and let $A' \subseteq B'$ be a simplicial subset. We wish to show that every lifting problem

$\xymatrix@C =50pt{ A' \ar [d] \ar [r] & \operatorname{Fun}(B,X) \ar [d]^{q'} \\ B' \ar [r] \ar@ {-->}[ur] & \operatorname{Fun}(A,X) \times _{ \operatorname{Fun}(A,S) } \operatorname{Fun}(B,S) }$

admits a solution. Unwinding the definitions, we are reduced to the problem of solving an associated lifting problem

$\xymatrix@C =50pt{ (A \times B') \coprod _{ (A \times A') } (B \times A') \ar [d] \ar [r] & X \ar [d]^{q} \\ B \times B' \ar [r] \ar@ {-->}[ur] & S. }$

The left vertical map in this diagram is a categorical equivalence by virtue of Corollary 4.5.4.15, so the existence of the desired solution follows from our assumption that $q$ is an isofibration. $\square$