#
Homotopy Type Theory
natural transformation > history (Rev #5, changes)

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

## Contents

< natural transformation

~~
~~~~
~~

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

~~
~~## See also

~~
~~Category theory functor precategory functor

~~
~~## References

~~
~~HoTT Book

~~
~~
Revision on June 7, 2022 at 16:16:13 by
Anonymous?.
See the history of this page for a list of all contributions to it.