Kerodon

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

Proposition 4.1.4.5. Let $q: X \rightarrow S$ be a morphism of simplicial sets. Then $q$ is an inner fibration if and only if the induced map

\[ \rho : \operatorname{Fun}(\Delta ^2,X) \rightarrow \operatorname{Fun}(\Lambda ^{2}_{1},X) \times _{ \operatorname{Fun}(\Lambda ^{2}_{1},S) } \operatorname{Fun}(\Delta ^2,S) \]

is a trivial Kan fibration.

Proof. The “only if” direction follows from Proposition 4.1.4.4. For the converse, we observe that $\rho $ is a trivial Kan fibration if and only if $q$ has the right lifting property with respect to the inclusion map

\[ (\Delta ^ m \times \Lambda ^2_1) \coprod _{ \operatorname{\partial \Delta }^ m \times \Lambda ^2_1 } (\operatorname{\partial }\Delta ^ m \times \Delta ^2) \subseteq \Delta ^ m \times \Delta ^2 \]

for every nonnegative integer $m$. Since the collection of inner anodyne morphisms is generated (as a weakly saturated class) by such inclusions (Lemma 1.4.6.9), it follows that $q$ has the right lifting property with respect to all inner anodyne morphisms (Proposition 1.4.4.16) and is therefore an inner fibration (Proposition 4.1.3.1). $\square$