Proposition 4.6.9.16. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $f: X \rightarrow Y$ be a morphism of $\operatorname{\mathcal{C}}$. For every object $Z \in \operatorname{\mathcal{C}}$, the diagram of Kan complexes
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{Y/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \ar [d]^{\iota ^{\mathrm{R}}_{Y,Z}}_{\sim } & \operatorname{\mathcal{C}}_{f/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \ar [l]^{\sim } \ar [r] & \operatorname{\mathcal{C}}_{X/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \ar [d]^{\iota ^{\mathrm{R}}_{X,Z}}_{\sim } \\ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z) \ar [rr]^{ \circ [f] } & & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Z) } \]
commutes up to homotopy, where the vertical maps are the right-pinch inclusion morphisms of Construction 4.6.5.7.
Proof of Proposition 4.6.9.16.
It will suffice to show that there exists a morphism of Kan complexes
\[ \iota ^{\mathrm{R}}_{X,Y,Z}: \operatorname{\mathcal{C}}_{f/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \rightarrow \{ f\} \times _{\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y) } \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y,Z) \]
for which the diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{\mathcal{C}}_{Y/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \ar [d]^{\iota ^{\mathrm{R}}_{Y,Z}} & \operatorname{\mathcal{C}}_{f/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \ar [l] \ar [d]^{ \iota ^{\mathrm{R}}_{X,Y,Z} } \ar [r] & \operatorname{\mathcal{C}}_{X/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \ar [d]^{\iota ^{\mathrm{R}}_{X,Z}} \\ \operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z) & \{ f\} \times _{\operatorname{Hom}_{\operatorname{\mathcal{C}}}(Y,Z) } \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y,Z) \ar [l] \ar [r] & \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Z) } \]
commutes (in the category of simplicial sets).
We first observe that there is a unique morphism of simplicial sets $e: \Delta ^2 \times \operatorname{\mathcal{C}}_{f/} \rightarrow \Delta ^1 \star \operatorname{\mathcal{C}}_{f/}$ with the property that $e|_{ \Delta ^1 \times \operatorname{\mathcal{C}}_{f/} }$ is given by projection onto the first factor, and $e|_{ \{ 2\} \times \operatorname{\mathcal{C}}_{f/} }$ is given by projection onto the second factor. Note that the composite map
\[ \Delta ^2 \times \operatorname{\mathcal{C}}_{f/} \xrightarrow {e} \Delta ^1 \star \operatorname{\mathcal{C}}_{f/} \rightarrow \operatorname{\mathcal{C}} \]
can be identified with a morphism of simplicial sets $e': \operatorname{\mathcal{C}}_{f/} \rightarrow \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}})$. Unwinding the definition, we see that $e'$ restricts to a morphism of simplicial subsets
\[ \iota _{X,Y,Z}^{\mathrm{R}}: \operatorname{\mathcal{C}}_{f/} \times _{\operatorname{\mathcal{C}}} \{ Z\} \rightarrow \{ f\} \times _{\operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y) } \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y,Z) \subseteq \operatorname{Fun}(\Delta ^2, \operatorname{\mathcal{C}}) \]
having the desired properties.
$\square$