Commit 2020-11-23 13:47 a71901f2

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.