Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Remark 6.1.5.2. In the situation of Construction 6.1.5.1, let $\operatorname{\mathcal{C}}^{\operatorname{op}}$ be the opposite of the $2$-category $\operatorname{\mathcal{C}}$, so that we can identify $\eta $ and $\eta '$ with $2$-morphisms

\[ \eta ^{\operatorname{op}}: \operatorname{id}_{C^{\operatorname{op}}} \Rightarrow f^{\operatorname{op}} \circ g^{\operatorname{op}} \quad \quad \eta '^{\operatorname{op}}: \operatorname{id}_{D^{\operatorname{op}}} \Rightarrow f'^{\operatorname{op}} \circ g'^{\operatorname{op}}. \]

Then the $2$-morphism $c(\eta ,\eta ')^{\operatorname{op}}$ can be identified with the contraction $c( \eta '^{\operatorname{op}}, \eta ^{\operatorname{op}} )$, formed in the $2$-category $\operatorname{\mathcal{C}}^{\operatorname{op}}$. In other words, $c(\eta ,\eta ')$ can also be computed as the composition

\[ \operatorname{id}_{C} \xRightarrow {\eta } g \circ f \xRightarrow {\sim } (g \circ \operatorname{id}_{D}) \circ f \xRightarrow {\eta '} (g \circ (g' \circ f'))) \circ f \xRightarrow {\sim } (( g \circ g') \circ f') \circ f \xRightarrow {\sim } (g \circ g') \circ (f' \circ f). \]

This follows from the commutativity of the diagram

\[ \xymatrix@R =50pt@C=50pt{ & g \circ f \ar@ {=>}[dl]_{\operatorname{id}_ g \circ \lambda _{f}^{-1}}^{\sim } \ar@ {=>}[dr]^{ \rho _ g^{-1} \circ \operatorname{id}_ f}_{\sim } & \\ g \circ (\operatorname{id}_ D \circ f) \ar@ {=>}[d]_{\operatorname{id}_ g \circ (\eta ' \circ \operatorname{id}_ f)} \ar@ {=>}[rr]_{\sim }^{\alpha _{g, \operatorname{id}_ D, f}} & & (g \circ \operatorname{id}_ D) \circ f \ar@ {=>}[d]^{ (\operatorname{id}_ g \circ \eta ') \circ \operatorname{id}_ F} \\ g \circ ((g' \circ f') \circ f) \ar@ {=>}[rr]_{\sim }^{\alpha _{g,g' \circ f', f}} \ar@ {=>}[d]^{\sim }_{ \operatorname{id}_ g \circ \alpha ^{-1}_{g',f'f} } & & (g \circ (g' \circ f')) \circ f \ar@ {=>}[d]_{\sim }^{ \alpha _{g,g',f'} \circ \operatorname{id}_{f'} } \\ g \circ (g' \circ (f' \circ f)) \ar@ {=>}[dr]^{\sim }_{\alpha _{g,g', f' \circ f} } & & ((g \circ g') \circ f') \circ f \ar@ {=>}[dl]_{\sim }^{ \alpha ^{-1}_{g \circ g', f',f} }\\ & (g \circ g') \circ (f' \circ f) & } \]

in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(C,C)$. Here the upper triangle commutes by virtue of the triangle identity (Proposition 2.2.1.14), the middle square commutes by the naturality of the associativity constraints of $\operatorname{\mathcal{C}}$, and the lower region commutes by virtue of the pentagon identity.