## 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. ## See also ## [[Category theory in HoTT]] [[functor precategory]] [[functor]] ## References ## [[HoTT Book]] category: category theory