mathlib documentation

category_theory.limits.constructions.binary_products

Constructing binary product from pullbacks and terminal object. #

If a category has pullbacks and a terminal object, then it has binary products.

TODO: provide the dual result.