mathlib3

a71901f2 - feat(category_theory/limits): explicit binary product functor in Type (#5043)

feat(category_theory/limits): explicit binary product functor in Type (#5043) Adds `binary_product_functor`, the explicit product functor in Type, and `binary_product_iso_prod` which shows it is isomorphic to the one picked by choice (this is helpful eg to show Type is cartesian closed). I also edited the definitions a little to use existing machinery instead - this seems to make `simp` and `tidy` stronger when working with the explicit product cone; but they're definitionally the same as the old ones.