Commit 2024-03-14 22:18 532c33b8

feat: chosen finite products in a category (#11248) This PR introduces a class for categories with explicit choices of binary products and terminal objects, and introduces the associated (Cartesian) symmetric monoidal instance. The primary use of this class is to be able to define internal algebraic objects in categories with chosen finite products, while retaining good definitional properties of the products in question, primarily as a convenience. We introduce an instance of this new class for the category of types where the binary product is the usual type-theoretic product and the terminal object is PUnit. Future work will introduce an instance for other categories, especially the category of affine schemes which should make objects like group schemes more convenient. NOTE: In some sense this reverses the refactor done in https://github.com/leanprover-community/mathlib/pull/3995 but only in the particular case of binary products and terminal objects. Working with (nonexplicit) (co)limits is still the preferred way to work with (co)limits in abstract categories, and instances of ChosenFiniteProducts (and other similar classes which may be introduced in the future) should be carefully considered before they are introduced.