Showing changes from revision #1 to #2:
Added | Removed | Changed
Definition
< product category
For precategories and , their product is a precategory with and
Identities are defined by and composition by
Properties
Lemma 9.5.3
For precategories , the following types are equivalent?:
- Functors
- Functors
Proof. Given , for any we obviously have a functor . This gives a function . Next, for any , we have for any the morphisms .
These are the components of a natural transformation . Functoriality in is easy to check, so we have a functor .
Conversly, suppose given . Then for any and we have the object , giving a function . And for and , we have the morphism
in . Functoriality is again easy to check, so we have a functor Finally, it is also clear that these operations are inverses.
See also
Category theory precategory functor functor precategory
References
HoTT book