# Homotopy Type Theory natural transformation (Rev #1)

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