In a category, a product (also called a cartesian product) of two objects and is an object equipped with morphisms and , called projections, such that for any object equipped with maps and there exists a unique (called the pairing of and ) such that and .
More generally, for Set Cat any discrete category, an -indexed limit is a product of factors. If is a finite set we speak of a finite product. Notice that this includes the case of the empty set, the product over which is, if it exists, the terminal object of the category in question.
When they exist, products are unique up to unique canonical isomorphism, so we often say “the product.”
|type theory||category theory|
|natural deduction||universal construction|
This interactive demonstration in FinSet lets you type two sets and see a product, showing the unique map to it from a randomly chosen equipped with and . It also generates a second product, showing the unique canonical isomorphism between this and the first product.