Kerodon

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

Construction 6.1.5.1. Let $\operatorname{\mathcal{C}}$ be a $2$-category containing objects $C$, $D$, and $E$, together with $1$-morphisms

\[ f: C \rightarrow D \quad \quad f': D \rightarrow E \quad \quad g: D \rightarrow C \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'$. We let $c(\eta , \eta ')$ denote the $2$-morphism given by 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), \]

where the unlabeled isomorphisms are given by the unit and associativity constraints of $\operatorname{\mathcal{C}}$. We will refer to $c(\eta , \eta ')$ as the contraction of $\eta $ and $\eta '$.