For and two categories, the product category is the category whose
objects are ordered pairs with an object of and an object of : .
morphisms are ordered pairs :
composition of morphisms is defined componentwise by composition in and .
This operation is the cartesian product in the 1-category Cat.
We discuss cartesian products for categories in homotopy type theory.
Note: UFP 2013 calls a category a “precategory” and a univalent category a “category”, but here we shall refer to the standard terminology of “category” and “univalent category” respectively.
For categories and , their product is a category with and
Identities are defined by and composition by
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 .
Conversely, 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.
Textbook accounts:
Discussion in homotopy type theory:
Last revised on June 3, 2023 at 08:31:51. See the history of this page for a list of all contributions to it.