Constructing limits from products and equalizers.

If a category has all products, and all equalizers, then it has all limits. Similarly, if it has all finite products, and all equalizers, then it has all finite limits.

TODO: provide the dual result.

category_theory.limits.has_limit_of_has_products_of_has_equalizers.diagram

Corresponding to any functor F : J ⥤ C, we construct a new functor from the walking parallel pair of morphisms to C, given by the diagram

         s
∏_j F j ===> Π_{f : j ⟶ j'} F j'
         t

where the two morphisms s and t are defined componentwise:

In a moment we prove that cones over F are isomorphic to cones over this new diagram.

category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_hom

The morphism from cones over the walking pair diagram diagram F to cones over the original diagram F.

category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_inv

The morphism from cones over the original diagram F to cones over the walking pair diagram diagram F.

category_theory.limits.has_limit_of_has_products_of_has_equalizers.cones_iso

The natural isomorphism between cones over the walking pair diagram diagram F and cones over the original diagram F.

category_theory.limits.limits_from_equalizers_and_products

Any category with products and equalizers has all limits.

category_theory.limits.finite_limits_from_equalizers_and_finite_products

Any category with finite products and equalizers has all finite limits.