mathlib documentation

category_theory.limits.shapes.constructions.preserve_binary_products

Show that a functor F : C ⥤ D preserves binary products if and only if ⟨Fπ₁, Fπ₂⟩ : F (A ⨯ B) ⟶ F A ⨯ F B (that is, prod_comparison) is an isomorphism for all A, B.

(Implementation). Construct a cone for pair A B ⋙ F which we will show is limiting.

Equations