# Homotopy Type Theory natural transformation (Rev #3)

## Definition

For functors $F,G: A \to B$, a natural transformation $\gamma : F \to G$ consists of

• For each $a : A$, a morphism $\gamma_a: hom_B(F a,G a)$ called the components of $\gamma$ at $a$.
• For each $a,b:A$ and $f:hom_A(a,b)$, we have $G f \circ \gamma_a= \gamma_b \circ F f$ (the naturality axiom).

## Properties

It follows that the type of natural transformations from $F$ to $G$ is a set.

### Composites with functors

For functors $F : A \to B$ and $G,H : B \to C$ and a natural transformation $\gamma : G \to H$, the composite $(\gamma F) : G F \to H F$ is given by

• For each $a:A$, the component $\gamma_{F a}$.

Naturality is easy to check. Similarly, for $\gamma$ as above and $K : C \to D$, the composite $(K \gamma): K G \to K H$ is given by

• For each $b: B$, the component $K(\gamma_b)$.

### Lemma 9.2.8

For functors $F,G: A\to B$ and $H,K: B \to C$ and natural transformations $\gamma : F \to G$ and $\delta : H \to K$, we have

$(\delta G)(H \gamma) = (K \gamma) (\delta F).$

Proof. It suffices to check componentwise: at $a:A$ we have

\begin{aligned} ((\delta G)(H \gamma))_a &\equiv (\delta G)_a (H \gamma)_a \\ &\equiv \delta_{G a} \circ H(\gamma_a)\\ &= K(\gamma_a) \circ \delta_{F a} \qquad (by\ naturality\ of\ \delta) \\ &\equiv (K \gamma)_a \circ (\delta F)_a\\ &\equiv ((K \gamma)(\delta F))_a.\ \square \end{aligned}