In Lemma 2.1.3.4 of Higher Topos Theory, the statement of the lemma requires that the fibers are not only nonempty but contractible. However, in the proof, I don't see where contractibility is directly used, only the fact that the fibers are nonempty. There is one other place where contractibility is mentioned, "Since the boundary of this simplex maps entirely into the contractible kan complex $S_t$, it is possible to extend $f'$ to $X(n+1)$." However, I don't see how contractibility directly factors in, since that would only attest to the uniqueness of the extension. The existence of the extension comes from the fact that the inclusion $\partial \Delta^n \times \Delta^1 \subseteq X(n+1)$ is left anodyne and $S_t$ is a nonempty Kan complex and the fact that the map f' factors through the inclusion of $S_t$.

Please correct me if I'm wrong. Also, there is a relevant post on meta where I first asked if this question is appropriate, and I was greenlighted by Anton.

In Lemma 2.1.3.4 of Higher Topos Theory, the statement of the lemma requires that the fibers are not only nonempty but contractible. However, in the proof, I don't see where contractibility is directly used, only the fact that the fibers are nonempty. There is one other place where contractibility is mentioned, "Since the boundary of this simplex maps entirely into the contractible kan complex $S_t$, it is possible to extend $f'$ to $X(n+1)$." However, I don't see how contractibility directly factors in, since that would only attest to the uniqueness of the extension. The existence of the extension comes from the fact that the inclusion $\partial \Delta^n \times \Delta^1 \subseteq X(n+1)$ is left anodyne and $S_t$ is a nonempty Kan complex and the fact that the map f' factors through the inclusion of $S_t$.

Please correct me if I'm wrong. Also, there is a relevant post on meta where I first asked if this question is appropriate, and I was greenlighted by Anton.