[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