mathlib documentation

category_theory.limits.shapes.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.