Homotopy Type Theory
functor > history (Rev #1)
Definition
Let and be precategories. A functor consists of
- A function
- For each , a function , generally also denoted .
- For each , we have .
- For each and amd , we have
Properties
By induction on identity, a functor also preserves (See precategory).
See also
Category theory in HoTT natural transformation full functor faithful functor
References
HoTT Book
Revision on September 4, 2018 at 18:22:31 by
Ali Caglayan.
See the history of this page for a list of all contributions to it.