Homotopy Type Theory natural transformation > history (Rev #4)

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).

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

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

See also

Category theory functor precategory functor

References

HoTT Book