# Kerodon

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

Proposition 4.2.4.1. Let $f: X_{} \rightarrow S_{}$ be a morphism of simplicial sets. Then:

• The morphism $f$ is a left fibration if and only if the evaluation map

$\operatorname{ev}_{0}: \operatorname{Fun}( \Delta ^1, X) \rightarrow \operatorname{Fun}( \{ 0\} , X) \times _{ \operatorname{Fun}( \{ 0\} , S)} \operatorname{Fun}( \Delta ^1, S)$

is a trivial Kan fibration.

• The morphism $f$ is a right fibration if and only if the evaluation map

$\operatorname{ev}_{1}: \operatorname{Fun}( \Delta ^1, X) \rightarrow \operatorname{Fun}( \{ 1\} , X) \times _{ \operatorname{Fun}( \{ 1\} , S)} \operatorname{Fun}( \Delta ^1, S)$

is a trivial Kan fibration.

Proof. We prove the second assertion; the first follows by passing to opposite simplicial sets. If $f$ is a right fibration, then the evaluation map $\operatorname{ev}_1$ is a trivial Kan fibration by virtue of Proposition 4.2.3.4 (since the inclusion $\{ 1\} \hookrightarrow \Delta ^1$ is right anodyne). Conversely, suppose that $\operatorname{ev}_1$ is a trivial Kan fibration. Then every lifting problem

$\xymatrix@C =100pt{ ( \Delta ^1 \times \Lambda ^{n}_{i} ) \coprod _{ \{ 1\} \times \Lambda ^ n_ i} (\{ 1\} \times \Delta ^ n ) \ar [r] \ar [d] & X_{} \ar [d]^{f} \\ \Delta ^1 \times \Delta ^ n \ar [r] \ar@ {-->}[ur] & S_{} }$

admits a solution. In other words, $f$ has the right lifting property with respect to the inclusion map

$u: ( \Delta ^1 \times \Lambda ^{n}_{i} ) \coprod _{ \{ 1\} \times \Lambda ^ n_ i} (\{ 1\} \times \Delta ^ n ) \hookrightarrow \Delta ^1 \times \Delta ^ n.$

If $0 < i \leq n$, then the horn inclusion $u_0: \Lambda ^ n_ i \hookrightarrow \Delta ^ n$ is a retract of $u$ (Lemma 3.1.2.8). It follows that $f$ also has the right lifting property with respect to $u_0$ (Proposition 1.4.4.9): that is, every lifting problem

$\xymatrix@R =50pt@C=50pt{ \Lambda ^{n}_{i} \ar [r]^-{\sigma _0} \ar [d] & X_{} \ar [d]^{f} \\ \Delta ^{n} \ar@ {-->}[ur]^-{\sigma } \ar [r]^-{ \overline{\sigma } } & S_{} }$

admits a solution. $\square$