Constructing binary product from pullbacks and terminal object. #
If a category has pullbacks and a terminal object, then it has binary products.
TODO: provide the dual result.
theorem
has_binary_products_of_terminal_and_pullbacks
(C : Type u)
[𝒞 : category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_pullbacks C] :
Any category with pullbacks and terminal object has binary products.