Remark 4.6.9.17. In the situation of Proposition 4.6.9.16, the morphisms
\[ \iota ^{\mathrm{R}}_{Y,Z}: \operatorname{\mathcal{C}}_{Y/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z) \quad \quad \iota ^{\mathrm{R}}_{X,Z}: \operatorname{\mathcal{C}}_{X/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \rightarrow \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Z) \]
are homotopy equivalences, by virtue of Proposition 4.6.5.10. Moreover, the restriction map $\operatorname{\mathcal{C}}_{f/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \rightarrow \operatorname{\mathcal{C}}_{Y/} \times _{\operatorname{\mathcal{C}}} \{ Z\} $ is a trivial Kan fibration (Corollary 4.3.6.14). Consequently, the precomposition map $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z) \xrightarrow { \circ [f]} \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Z)$ is characterized (up to homotopy) by the conclusion of Proposition 4.6.9.16.