Homotopy Type Theory
natural transformation > history (Rev #5, changes)
Showing changes from revision #4 to #5:
Added | Removed | Changed
Contents
< natural transformation
Definition
For functors , a natural transformation consists of
- For each , a morphism called the components of at .
- For each and , we have (the naturality axiom).
Properties
It follows that the type of natural transformations from to is a set.
Composites with functors
For functors and and a natural transformation , the composite is given by
- For each , the component .
Naturality is easy to check. Similarly, for as above and , the composite is given by
- For each , the component .
Lemma 9.2.8
For functors and and natural transformations and , we have
Proof. It suffices to check componentwise: at we have
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.