Let $f:x\to z$ and $g:y\to z$ be morphisms in an $\infty$-category $\mathcal C$. It seems that the square
$$\require{AMScd}
\begin{CD}
\operatorname{Map}\_{\mathcal C\_{/z}}(f,g) @>>> \operatorname{Map}\_{\mathcal C^{\Delta^1}}(f,g)\\
@VVV @VVV \\
\Delta^0 @>{\operatorname{id}\_z}>> \operatorname{Map}\_{\mathcal C}(z,z)
\end{CD}$$
should be (homotopy-)cartesian in the $\infty$-category of spaces. If this is indeed true, does anyone have a reference or a proof?



Maps in the slice category vs. maps in the arrow category
Let us use the fat slice $\mathcal{C}^{z/}$ (See HTT, $\S$4.2.1) and the model $\operatorname{Hom}\_{\mathcal{C}}(x,y)=\operatorname{Fun}(\Delta^1,\mathcal{C})\times \_{\mathcal{C}\times \mathcal{C}}\{(x,y)\}$ of the mapping space. By computation, we can check that the square


$$\require{AMScd}
\begin{CD}
\operatorname{Hom}\_{\mathcal{C}^{/z}}(f,g) @>>> \operatorname{Hom}\_{\operatorname{Fun}(\Delta^1,\mathcal{C})}(f,g)\\
@VVV @VVV \\
\Delta^0 @>{\operatorname{id}\_z}>> \operatorname{Hom}\_{\mathcal{C}}
(z,z)\end{CD}$$


is cartesian. The right vertical arrow is a Kan fibration, because $\operatorname{ev}\_1:\operatorname{Fun}(\Delta^1,\mathcal{C})\to\mathcal{C}$ is an inner fibration. (In general, inner fibrations induce Kan fibrations between various mapping spaces. See, e.g., Lemma 2.4.4.1. The lemma talks about the usual slice, but the proof applies to fat slice as well.) So the above square is homotopy cartesian.


