Kerodon

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

Proposition 2.2.1.14 (The Triangle Identity). Let $\operatorname{\mathcal{C}}$ be a $2$-category containing a pair of $1$-morphisms $f: X \rightarrow Y$ and $g: Y \rightarrow Z$. Then the diagram of $2$-morphisms

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

is commutative.

Proof. We have a diagram of isomorphisms

\[ \xymatrix@R =50pt@C=-17pt{ & g \circ ( (\operatorname{id}_ Y \circ \operatorname{id}_ Y) \circ f) \ar [rr]^{\alpha } \ar [d]^{\upsilon _ Y} & & (g \circ ( \operatorname{id}_ Y \circ \operatorname{id}_ Y ) ) \circ f \ar [d]_{\upsilon _{Y} } \ar [ddr]^{\alpha } & \\ & g \circ (\operatorname{id}_ Y \circ f) \ar [rr]^{ \alpha } \ar [d]^{\alpha } & & (g \circ \operatorname{id}_ Y) \circ f \ar [dll]^{ \operatorname{id}} & \\ g \circ (\operatorname{id}_ Y \circ (\operatorname{id}_ Y \circ f) ) \ar [uur]^{\alpha } \ar [ur]_{\lambda _ f} \ar [drr]^{ \alpha } & (g \circ \operatorname{id}_ Y) \circ f \ar [r]^-{ \rho _{g}} & g \circ f & g \circ ( \operatorname{id}_ Y \circ f) \ar [l]_-{ \lambda _ f} \ar [u]^{ \alpha } & ((g \circ \operatorname{id}_ Y) \circ \operatorname{id}_ Y) \circ f \ar [ul]^{\rho _ g} \\ & & (g \circ \operatorname{id}_ Y) \circ (\operatorname{id}_ Y \circ f). \ar [ul]_{ \lambda _ f } \ar [ur]^{ \rho _ g } \ar [urr]^{ \alpha } & & } \]

Here the outer cycle commutes by the pentagon identity $(P)$ of Definition 2.2.1.1, the upper rectangle by the functoriality of the associativity constraint, the upper side triangles by the definition of the left and right unit constraints, the quadrilaterals on the lower sides by the functoriality of the associativity constraints, and the lower region by the functoriality of composition. It follows that the middle square is also commutative, which is equivalent to the statement of Proposition 2.2.1.14. $\square$