mathlib documentation

category_theory.limits.preserves.shapes.binary_products

Preserving binary products #

Constructions to relate the notions of preserving binary products and reflecting binary products to concrete binary fans.

In particular, we show that prod_comparison G X Y is an isomorphism iff G preserves the product of X and Y.