# Commit 2020-11-23 13:47 a71901f2

View on Github →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.