Composition map in $\infty$-categories Let $\mathcal{C}$ be an $\infty$-category, and let $u:x\rightarrow y$ be an edge. It seems reasonable to say that: The map $Map_{\mathbb{C}[\mathcal{C}]}(a,x)\rightarrow Map_{\mathbb{C}[\mathcal{C}]}(a,y)$ given by composition with $u\in Map_{\mathbb{C}[\mathcal{C}]}(x,y)_0$, where $\mathbb{C}[\mathcal{C}]$ is the simplical category associated to $\mathcal{C}$, is equivalent in the homotopy category of simplicial sets to the composite $\mathcal{C}_{\backslash x}\times_{\mathcal{C}}\{a\}\rightarrow \mathcal{C}_{\backslash u}\times_{\mathcal{C}}\{a\} \rightarrow \mathcal{C}_{\backslash y}\times_{\mathcal{C}}\{a\}$, where the first map is a section of the trivial fibration $\mathcal{C}_{\backslash x}\times_{\mathcal{C}}\{a\}\leftarrow \mathcal{C}_{\backslash u}\times_{\mathcal{C}}\{a\}$.
However, I am unable to come up with a proof, and have not found one in HTT. I would guess that one needs to use the straightening functor, as is done to identify the targets, but how to deal with the composition map of the simplicial category associated to $\mathcal{C}$?
EDIT: I am relatively convinced that it boils down to proving that the maps: $$(St_{\mathcal{C}}\mathcal{C}_{/f})(a)\rightarrow (St_{\mathcal{C}}\mathcal{C}_{/x})(a)\rightarrow Map_{\mathbb{C}[\mathcal{C}]}(a,x)\rightarrow Map_{\mathbb{C}[\mathcal{C}]}(a,y)$$ and $$(St_{\mathcal{C}}\mathcal{C}_{/f})(a)\rightarrow (St_{\mathcal{C}}\mathcal{C}_{/y})(a)\rightarrow Map_{\mathbb{C}[\mathcal{C}]}(a,y)$$ are homotopic, where $(St_{\mathcal{C}}\mathcal{C}_{/x})(a)\rightarrow Map_{\mathbb{C}[\mathcal{C}]}(a,x)$ corresponds to the map $f''$ in HTT 2.2.4 but I do not see any reasonnable way to proceed.
 A: Here's one way to do this. Consider the left fibration $p\colon C_{a/}\to C$, and pick a lift of $u\colon x\to y$ (let's assume that there is a map $a\to x $ otherwise it's trivial). When you have a cocartesian fibration $p\colon E \to B$, a $p$-cocartesian lift of a morphism $u\colon x \to y$ in the base category $B$  induce a map between the fibers $E_x \to E_y$ which is equivalent to the action of the functor $St(p)\colon B \to Set^+_{\Delta}$ applied to $u$ (in our simpler case, the map is a left fibration so this follows more or less from 2.1.1.4 in HTT). The map you mentioned is equivalent to the one you obtain in this way, so we are left with analyzing what the action of $St(p)(u)$ is. This is defined by $u\circ -\colon \mathfrak{C}(\bar{C})(*,x)\to \mathfrak{C}(\bar{C})(*,y)$, where $\bar{C}$ is the pushout of $\mathfrak{C}(C_{a/}) \to \mathfrak{C}(C^{\lhd}_{a/}) $ and $ \mathfrak{C}(C_{a/}) \to \mathfrak{C}(C)$. Since $\mathfrak{C}(C_{a/}) \to \mathfrak{C}(C^{\lhd}_{a/}) $ is a trivial cofibration, we can identify  $\mathfrak{C}(\bar{C})(*,x)$ with $\mathfrak{C}(C)(a,x)$, and similarly for $y$, which concludes the proof.
A: I had also been wondering about this for a while. I think I've figured this out.
First we observe that $\operatorname{St}_{\mathcal{C}}(\{x\})=\mathfrak{C}[\mathcal{C}](-,x)$; this follows by directly constructing the pushout $\mathfrak{C}[\mathcal{C}\amalg_{\{x\}}(\{x\}^\triangleright)]$.
Now recall (Proposition 2.2.3.15) that there is a weak homotopy equivalence
$$|\mathcal{E}_x|_{Q^{\bullet}}\to\operatorname{St}(\mathcal{E})(x)$$
for any right fibration $\mathcal{E}$ and $x\in\mathcal{C}_0$. This is natural in $\mathcal{E}$, so it suffices to show that there is a weak equivalence $\operatorname{St}(\mathcal{C}_{/x})\to\operatorname{St}(\{x\})=\mathfrak{C}[\mathcal{C}](-,x)$ making the diagram
$$
\require{AMScd}
\begin{CD}
\operatorname{St}(\mathcal{C}_{/x}) @<<< \operatorname{St}(\mathcal{C}_{/f}) @>>>\operatorname{St}(\mathcal{C}_{/y
})\\
@VVV @. @VVV\\
\operatorname{St}(\{x\})@= \operatorname{St}(\{x\}) @>>{f_\ast}> \operatorname{St}(\{y\})
\end{CD}
$$
commutative in the homotopy category.
Consider the counit $(\mathcal{C}_{/x})^\triangleright\to\mathcal{C}$ of the slice-join adjunction. This map and the identity of $\mathcal{C}$ gives us a map $\mathcal{C}\amalg_{\mathcal{C}_{/x}}(\mathcal{C}_{/x})^\triangleright\to\mathcal{C}.$ It is easy to check that the induced map $\operatorname{St}(\mathcal{C}_{/x})\to\mathfrak{C}[\mathcal{C}](-,x)$ is a retraction of the weak equivalence $\operatorname{St}(\{x\})\to\operatorname{St}(\mathcal{C}_{/x})$. We claim that this map does the job. Consider the $2$-simplex $\sigma = s_0 f$, which corresponds to the triangle
$$
\begin{array}{ccccccccc} 
x & \xrightarrow{1_x} & x\\
 & \searrow & \downarrow\\
 &&y.
\end{array}
$$
Then there is a commutative diagram
$$
\begin{array}{ccccccccc} 
\mathcal{C}_{/x} & \leftarrow  & \mathcal{C}_{/f} & \rightarrow & \mathcal{C}_{/y}  \\
\uparrow & & \uparrow  & \nearrow & \\
\{x\} & = & \{x\}  
\end{array}
$$
over $\mathcal{C}, $ where the upward-pointing arrows are $1_x$, $\sigma$, and $f$ respectively. One can verify that the diagram
$$
\begin{array}{ccccccccc} 
& \operatorname{St}(\mathcal{C}_{/y})\\
\nearrow & \downarrow \\
\operatorname{St}(\{x\})  \xrightarrow{f_\ast} & \operatorname{St}(\{y\})
\end{array}
$$
is also commutative. The claim follows.
