[05VR]
Proposition 11.4 . Let f , g ∈ map ( x , y ) f,g\in\map(x,y) f ∼ g f\sim g f ∗ , g ∗ : map ( w , x ) → map ( w , y ) f_{*},g_{*}\colon\map(w,x)\rightarrow\map(w,y) w ∈ ob W w\in{\operatorname{ob}}W f ∗ , g ∗ : map ( y , z ) → map ( x , z ) f^{*},g^{*}\colon\map(y,z)\rightarrow\map(x,z) z ∈ ob W z\in{\operatorname{ob}}W
[05VS]
Proof. The only if direction is straightforward. To prove the if direction,
suppose that f ∗ f_{*} g ∗ g_{*} w ∈ ob W w\in{\operatorname{ob}}W w = x w=x f ∗ ( id x ) ∼ f f_{*}(\id_{x})\sim f
map ( x , x ) \displaystyle{{\map(x,x)}\ignorespaces\ignorespaces\ignorespaces\ignorespaces} { f } × 1 \scriptstyle{\{f\}\times 1} pt \displaystyle{{{\operatorname{pt}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces} { id x } \scriptstyle{\{\id_{x}\}} { f } \scriptstyle{\{f\}} map ( x , y ) × map ( x , x ) \displaystyle{{\map(x,y)\times\map(x,x)}} map ( x , y ) \displaystyle{{\map(x,y)}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces} 1 × { id x } \scriptstyle{1\times\{\id_{x}\}} s 0 \scriptstyle{s_{0}} 1 \scriptstyle{1} map ( x , x , y ) \displaystyle{{\map(x,x,y)}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces} ∼ \scriptstyle{\sim} ( d 0 , d 2 ) \scriptstyle{(d_{0},d_{2})} d 1 \scriptstyle{d_{1}} map ( x , y ) \displaystyle{{\map(x,y)}}
Similarly g ∗ ( id x ) ∼ g g_{*}(\id_{x})\sim g f ∼ g f\sim g 11.3