Proposition 6.1.5.3. Let $\operatorname{\mathcal{C}}$ be a $2$-category containing objects $C$, $D$, and $E$, together with $1$-morphisms
\[ f: C \rightarrow D \quad \quad g: D \rightarrow C \quad \quad f': D \rightarrow E \quad \quad g': E \rightarrow D \]
and $2$-morphisms $\eta : \operatorname{id}_{C} \Rightarrow g \circ f$ and $\eta ': \operatorname{id}_{D} \Rightarrow g' \circ f'$. Let $T$ be another object of $\operatorname{\mathcal{C}}$ equipped with $1$-morphisms $c: T \rightarrow C$ and $e: T \rightarrow E$. Then the diagram
6.1
\begin{equation} \begin{gathered}\label{equation:contraction-compose-adjuncts} \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,E)}( (f' \circ f) \circ c, e ) \ar [dd] \ar [r]_{\sim }^{\alpha _{f',f,c}} & \operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,E)}( f' \circ (f \circ c), e ) \ar [d] \\ & \operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,D)}( f \circ c, g' \circ e ) \ar [d] \\ \operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,C)}( c, (g \circ g') \circ e ) \ar [r]^-{\alpha _{g,g',e}}_{\sim } & \operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,C)}( c, g \circ (g' \circ e) ) } \end{gathered} \end{equation}
is commutative. Here the right vertical maps are given by the formation of right adjuncts with respect to $\eta $ and $\eta '$ (in the sense of Construction 6.1.2.1), while the left vertical map is given by the formation of right adjuncts with respect to the contraction $c(\eta ,\eta ')$ of Construction 6.1.5.1.
Proof.
Fix a $2$-morphism $\beta : (f'\circ f) \circ c \Rightarrow e$ in $\operatorname{\mathcal{C}}$. Clockwise and counterclockwise composition around the outside of the diagram (6.1) determines two elements of $\operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,C)}( c, (g \circ g') \circ e)$, and we wish to prove that these two elements are the same. Unwinding the definitions, we see that these elements can be obtained as the vertical composition of $c \xRightarrow [\sim ]{\lambda _{c}^{-1}} \operatorname{id}_{C} \circ c \xRightarrow {\eta \circ \operatorname{id}_ c} (g\circ f) \circ c$ with $2$-morphisms given by clockwise and counterclockwise composition around the outside of the diagram
\[ \xymatrix@R =50pt@C=50pt{ (gf)c \ar@ {=>}[d]_-{ \lambda _{f}^{-1} }^{\sim } \ar@ {=>}[r]^{\sim } & g (f c) \ar@ {=>}[d]_-{\lambda _{f}^{-1}}^{\sim } \ar@ {=>}[dr]^-{ \lambda _{f c}^{-1}}_{\sim } & & \\ (g (\operatorname{id}_ D f)) c \ar@ {=>}[d]^-{\eta '} \ar@ {=>}[r]^{\sim } & g ((\operatorname{id}_ D f) c) \ar@ {=>}[r]^{\sim } \ar@ {=>}[d]^-{\eta '} & g (\operatorname{id}_ D (f c)) \ar@ {=>}[d]^-{\eta '} & \\ (g ((g' f') f)) c \ar@ {=>}[d]^-{\sim } \ar@ {=>}[r]^{\sim } & g (((g' f') f) c) \ar@ {=>}[d]^-{\sim } \ar@ {=>}[r]^{\sim } & g ((g' f') (f c)) \ar@ {=>}[r]^{\sim } & g (g' (f' (f c))) \ar@ {=>}[dl]^{\sim } \\ (g(g'(f'f)))c \ar@ {=>}[d]^-{\sim } \ar@ {=>}[r]^{\sim } & g ((g' (f' f)) c) \ar@ {=>}[r]^{\sim } & g (g' ((f' f) c) ) \ar@ {=>}[d]^-{\sim } \ar@ {=>}[r]^{\beta } & g (g' e) \ar@ {=>}[d] \\ ( (g g') (f' f) ) c \ar@ {=>}[rr]^{\sim } & & (g g') (( f' f) c) \ar@ {=>}[r]^{\beta } & (g g') e} \]
in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T, C)$; here denote the composition of $1$-morphisms $u$ and $v$ in $\operatorname{\mathcal{C}}$ by $uv$ (rather than $u \circ v$) to simplify the notation, and the unlabeled isomorphisms are given by the associativity constraints of $\operatorname{\mathcal{C}}$. It will therefore suffice to observe that this diagram is commutative. The commutativity of the pentagonal regions follows from the pentagon identity in $\operatorname{\mathcal{C}}$, the commutativity of the triangle from Proposition 2.2.1.16, and the commutativity of each square from the naturality of the associativity constraints of $\operatorname{\mathcal{C}}$.
$\square$