mathlib documentation

category_theory.limits.constructions.binary_products

Constructing binary product from pullbacks and terminal object. #

The product is the pullback over the terminal objects. In particular, if a category has pullbacks and a terminal object, then it has binary products.

We also provide the dual.