Lemma 2.1.1.4 in Lurie's HTT

Question

I have encountered a problem in understanding Lurie's proof of the following fact:

"Given a left fibration between simplicial sets $q:X \to S$, there exists a functor $$ho(S) \to Ho(sSet)$$ which is defined as follows: a point $s \in S$ is sent to the fiber $X_s$ of $q$ over $s$, and an arrow $f:s \to s'$ in $S'$ is sent to the homotopy class of a lift in

restricted to $\{1\} \times X_s$, which will be denoted by $f_!:X_s \to X_{s'}$".

The author wants to characterize the map $$[f_!]\circ (\cdot): Ho(sSet)(\cdot, X_s) \to Ho(sSet)(\cdot, X_{s'})$$ so as to obtain the desired result (except for the independence from the homotopy class of $f$, which I guess is left to the reader).

The problem is I don't see why it holds that, given a $K\in sSet$ and arrows $\eta:K \to X_s, \ \eta':K \to X_{s'}$, $$\eta'\simeq f_! \circ \eta \iff \exists p:K \times \Delta[1] \to X$$ such that $p_{|K \times \{0\}}\simeq \eta, \ p_{|K \times \{1\}}\simeq \eta'$ and $$q \circ p= K \times \Delta[1] \to \Delta[1] \to S$$ where the last arrow is $f$.

Thanks in advance for any help, which will of course be highly appreciated.

Answer 1

Consider the diagram

where the top left horizontal arrow is given by $\eta$. Observe that homotopy classes of lifts of the map $X_s \times \Delta^1 \rightarrow S$ are the same as homotopy classes of lifts of the map $K \times \Delta^1 \rightarrow S$. This follows from the same argument showing that the homotopy class of $f_!$ only depends on $f$, together with the fact that the left hand square is a pullback. (I'll include the argument below for completeness).

Given that, we're done. A lift of $K \times \Delta^1 \rightarrow S$ is precisely the map $p$ as stated, and the above observation says the lift is homotopic to the composition $K \times \Delta^1 \rightarrow X_s \times \Delta^1 \rightarrow X$, which is the same as saying that $[\eta'] = [f_!] \circ [\eta]$.

---

Okay, now for the promised argument which says that homotopy classes of lifts in a diagram like

only depend on the map $f$. But such a lift is equivalent to a section of $X \times_S (Y \times \Delta^1)$ over $Y \times \Delta^1$ which is specified at $Y \times \{0\}$. This pullback may be obtained by first pulling back $X$ to $\Delta^1$, where the fibration trivializes up to homotopy. Thus $X \times_S(Y \times \Delta^1)$ is trivial up to homotopy so that sections are determined up to homotopy by maps $Y \times \Delta^1 \rightarrow X_s$. Since we've already specified the map on $Y \times \{0\}$, there is only one extension up to homotopy as $Y \times \{0\} \rightarrow Y \times \Delta^1$ is an equivalence.