Remark 3.1.5.3 (Homotopy Extension Lifting Property). Let $f: X \rightarrow S$ be a Kan fibration of simplicial sets. Suppose we are given a morphism of simplicial sets $u: B \rightarrow X$ and a homotopy $\overline{h}$ from $f \circ u$ to another map $\overline{v}: B \rightarrow S$. Then we can choose a map of simplicial sets $h: \Delta ^1 \times B_{} \rightarrow X_{}$ satisfying $f \circ h = \overline{h}$ and $h|_{ \{ 0\} \times B_{} } = u$: in other words, $\overline{h}$ can be lifted to a homotopy $h$ from $u$ to another map $v = h|_{ \{ 1\} \times B_{} }$. Moreover, given any simplicial subset $A_{} \subseteq B_{}$ and any map $h_0: \Delta ^1 \times A_{} \rightarrow X_{}$ satisfying $f \circ h_0 = \overline{h}|_{ \Delta ^1 \times A_{}}$ and $h_0|_{ \{ 0\} \times A_{} } = u|_{ A_{}}$, we can arrange that $h$ is an extension of $h_0$. This follows from Theorem 3.1.3.1, which guarantees that the restriction map
is a Kan fibration (and therefore weakly right orthogonal to the inclusion $\{ 0\} \hookrightarrow \Delta ^1$). For a partial converse, see Corollary 4.2.6.2.