mathlib3

928496ad - feat(category_theory/limits) Binary product from pullbacks and terminal object (#1998)

feat(category_theory/limits) Binary product from pullbacks and terminal object (#1998) * Binary product from pullbacks and terminal object * Update binary_products.lean * simplifications * pare down the proof a bit more * changes from review * adjust simp to rw Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>