mathlib

a87f62bc - feat(category_theory/limits/preserves): preserving binary products (#5061)

feat(category_theory/limits/preserves): preserving binary products (#5061) This moves and re-does my old file about preserving binary products to match the new API and framework for preservation of special shapes, and also cleans up some existing API. (I can split this up if necessary but they're all pretty minor changes, so hope this is okay!)