#
Homotopy Type Theory

natural transformation (changes)

Showing changes from revision #3 to #4:
Added | ~~Removed~~ | ~~Chan~~ged

## Contents

## 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).~~**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}$

## See also

Category theory functor precategory functor

## References

HoTT Book

Last revised on September 6, 2018 at 18:11:34.
See the history of this page for a list of all contributions to it.