The Clowder Project

Let $\mathcal{C}$, $\mathcal{D}$, and $\mathcal{E}$ be categories.

1. 1.

   Functionality. The assignment $(\beta ,\alpha )\mapsto \beta \circ \alpha $ defines a function

   \[ \circ _{F,G,H}\colon \operatorname {\mathrm{Nat}}(G,H)\times \operatorname {\mathrm{Nat}}(F,G)\to \operatorname {\mathrm{Nat}}(F,H). \]
2. 2.

   Associativity. Let $F,G,H,K\colon \mathcal{C}\overset {\rightrightarrows }{\rightrightarrows }\mathcal{D}$ be functors. The diagram

   
   commutes, i.e. given natural transformations
   \[ F\mathbin {\overset {\alpha }{\Longrightarrow }}G\mathbin {\overset {\beta }{\Longrightarrow }}H\mathbin {\overset {\gamma }{\Longrightarrow }}K, \]

   we have

   \[ (\gamma \circ \beta )\circ \alpha =\gamma \circ (\beta \circ \alpha ). \]
3. 3.

   Unitality. Let $F,G\colon \mathcal{C}\rightrightarrows \mathcal{D}$ be functors.

   1. (a)

      Left Unitality. The diagram

      
      commutes, i.e. given a natural transformation $\alpha \colon F\Longrightarrow G$, we have
      \[ \operatorname {\mathrm{id}}_{G}\circ \alpha =\alpha . \]
   2. (b)

      Right Unitality. The diagram

      
      commutes, i.e. given a natural transformation $\alpha \colon F\Longrightarrow G$, we have
      \[ \alpha \circ \operatorname {\mathrm{id}}_{F}=\alpha . \]
4. 4.

   Middle Four Exchange. Let $F_{1},F_{2},F_{3}\colon \mathcal{C}\to \mathcal{D}$ and $G_{1},G_{2},G_{3}\colon \mathcal{D}\to \mathcal{E}$ be functors. The diagram

   
   commutes, i.e. given a diagram
   
   in $\mathsf{Cats}_{\mathsf{2}}$, we have
   \[ (\beta '\mathbin {\star }\alpha ')\circ (\beta \mathbin {\star }\alpha )=(\beta '\circ \beta )\mathbin {\star }(\alpha '\circ \alpha ). \]
5. 5.

   Interaction With Natural Isomorphisms. If $\alpha $ and $\beta $ are natural isomorphisms, then so is $\beta \circ \alpha $.