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

## See also

Category theory in HoTT functor precategory functor

## References

HoTT Book

Revision on September 4, 2018 at 14:22:49 by
Ali Caglayan.
See the history of this page for a list of all contributions to it.