Example 3.1.7.10 (Path Fibrations). If $f: X \rightarrow Y$ is a morphism of Kan complexes, then we can give a much more explicit proof of Proposition 3.1.7.1. Let $P(f)$ denote the fiber product $X \times _{ \operatorname{Fun}( \{ 0\} , Y)} \operatorname{Fun}( \Delta ^1, Y)$. Then $f$ factors as a composition $X \xrightarrow {f'} P(f) \xrightarrow {f''} Y$, where $f''$ is given by evaluation at the vertex $\{ 1\} \subseteq \Delta ^1$ and $f'$ is obtained by amalgamating the identity morphism $\operatorname{id}_{X}$ with the composition $X \xrightarrow {f} Y \xrightarrow {\delta } \operatorname{Fun}( \Delta ^1, Y)$. Moreover:

The morphism $f'$ is a section of the projection map $P(f) \rightarrow X$, which is a pullback of the evaluation map $\operatorname{Fun}( \Delta ^1, Y) \rightarrow \operatorname{Fun}( \{ 0\} , Y)$ and therefore a trivial Kan fibration (Corollary 3.1.3.6). It follows that $f'$ is a weak homotopy equivalence. Since it is also a monomorphism, it is anodyne (see Corollary 3.3.7.5).

The morphism $f''$ factors as a composition

\[ P(f) = X \times _{ \operatorname{Fun}( \{ 0\} , Y)} \operatorname{Fun}(\Delta ^1, Y) \xrightarrow {u} X \times \operatorname{Fun}(\{ 1\} , Y) \xrightarrow {v} Y, \]where $u$ is a pullback of the restriction map $\operatorname{Fun}(\Delta ^1, Y) \rightarrow \operatorname{Fun}(\operatorname{\partial \Delta }^{1}, Y)$ (and therefore a Kan fibration by virtue of Corollary 3.1.3.3) and $v$ is a pullback of the projection map $X \rightarrow \Delta ^0$ (and therefore a Kan fibration by virtue of our assumption that $X$ is a Kan complex). It follows that $f''$ is also a Kan fibration.