Kerodon

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

Construction 6.1.5.7. 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 $\epsilon : f \circ g \Rightarrow \operatorname{id}_{D}$ and $\epsilon ': f' \circ g' \Rightarrow \operatorname{id}_{E}$ be $2$-morphisms of $\operatorname{\mathcal{C}}$. We let $c( \epsilon , \epsilon ')$ denote the $2$-morphism given by the composition

\[ (f' \circ f) \circ (g \circ g') \xRightarrow {\sim } f' \circ (f \circ (g \circ g')) \xRightarrow {\sim } f' \circ ((f \circ g) \circ g') \xRightarrow {\epsilon } f' \circ (\operatorname{id}_{D} \circ g') \xRightarrow {\sim } f' \circ g' \xRightarrow {\epsilon '} \operatorname{id}_{E} \]

We will refer to $c(\epsilon ,\epsilon ')$ as the contraction of $\epsilon $ and $\epsilon '$.