Homotopy Type Theory
functor > history (Rev #2, changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
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 19:28:42 by
Ali Caglayan.
See the history of this page for a list of all contributions to it.