diff --git a/src/category_theory/limits/limits.lean b/src/category_theory/limits/limits.lean
index f94a94b768cf1..2f7049e2a586c 100644
--- a/src/category_theory/limits/limits.lean
+++ b/src/category_theory/limits/limits.lean
@@ -454,7 +454,7 @@ def limit.lift (F : J ⥤ C) [has_limit F] (c : cone F) : c.X ⟶ limit F :=
 @[simp] lemma limit.is_limit_lift {F : J ⥤ C} [has_limit F] (c : cone F) :
   (limit.is_limit F).lift c = limit.lift F c := rfl
 
-@[simp,reassoc] lemma limit.lift_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
+@[simp, reassoc] lemma limit.lift_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
   limit.lift F c ≫ limit.π F j = c.π.app j :=
 is_limit.fac _ c j
 
@@ -617,7 +617,7 @@ def lim : (J ⥤ C) ⥤ C :=
 
 variables {F} {G : J ⥤ C} (α : F ⟶ G)
 
-@[simp,reassoc] lemma lim.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
+@[simp, reassoc] lemma lim.map_π (j : J) : lim.map α ≫ limit.π G j = limit.π F j ≫ α.app j :=
 by apply is_limit.fac
 
 @[simp] lemma limit.lift_map (c : cone F) :
diff --git a/src/category_theory/limits/shapes/constructions/finite_limits.lean b/src/category_theory/limits/shapes/constructions/finite_limits.lean
new file mode 100644
index 0000000000000..1f83b95f3fff2
--- /dev/null
+++ b/src/category_theory/limits/shapes/constructions/finite_limits.lean
@@ -0,0 +1 @@
+-- TODO construct finite limits from finite products and equalizers
diff --git a/src/category_theory/limits/shapes/constructions/limits.lean b/src/category_theory/limits/shapes/constructions/limits.lean
new file mode 100644
index 0000000000000..e3d54ed670afb
--- /dev/null
+++ b/src/category_theory/limits/shapes/constructions/limits.lean
@@ -0,0 +1 @@
+-- TODO construct limits from products and equalizers
diff --git a/src/category_theory/monoidal/of_has_finite_products.lean b/src/category_theory/monoidal/of_has_finite_products.lean
new file mode 100644
index 0000000000000..449e98a777728
--- /dev/null
+++ b/src/category_theory/monoidal/of_has_finite_products.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Simon Hudon
+-/
+import category_theory.monoidal.category
+import category_theory.limits.shapes.finite_products
+import category_theory.limits.shapes.binary_products
+import category_theory.limits.shapes.terminal
+import category_theory.limits.types
+
+/-!
+# The natural monoidal structure on any category with finite (co)products.
+
+A category with a monoidal structure provided in this way is sometimes called a (co)cartesian category,
+although this is also sometimes used to mean a finitely complete category.
+(See https://ncatlab.org/nlab/show/cartesian+category.)
+
+As this works with either products or coproducts, we don't set up either construct as an instance.
+-/
+
+open category_theory.limits
+
+universes v u
+
+namespace category_theory
+
+section
+variables (C : Type u) [𝒞 : category.{v+1} C]
+include 𝒞
+
+local attribute [tidy] tactic.case_bash
+
+/-- A category with finite products has a natural monoidal structure. -/
+def monoidal_of_has_finite_products [has_finite_products.{v} C] : monoidal_category C :=
+{ tensor_unit  := terminal C,
+  tensor_obj   := λ X Y, limits.prod X Y,
+  tensor_hom   := λ _ _ _ _ f g, limits.prod.map f g,
+  associator   := prod.associator,
+  left_unitor  := prod.left_unitor,
+  right_unitor := prod.right_unitor }
+
+/-- A category with finite coproducts has a natural monoidal structure. -/
+def monoidal_of_has_finite_coproducts [has_finite_coproducts.{v} C] : monoidal_category C :=
+{ tensor_unit  := initial C,
+  tensor_obj   := λ X Y, limits.coprod X Y,
+  tensor_hom   := λ _ _ _ _ f g, limits.coprod.map f g,
+  associator   := coprod.associator,
+  left_unitor  := coprod.left_unitor,
+  right_unitor := coprod.right_unitor }
+
+end
+
+end category_theory
+
+-- TODO in fact, a category with finite products is braided, and symmetric,
+-- and we should say that here.
diff --git a/src/category_theory/monoidal/types.lean b/src/category_theory/monoidal/types.lean
index 9d4d3826e0679..bb661542dcd11 100644
--- a/src/category_theory/monoidal/types.lean
+++ b/src/category_theory/monoidal/types.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Jendrusch, Scott Morrison
 -/
 import category_theory.types
-import category_theory.monoidal.category
+import category_theory.limits.types
+import category_theory.monoidal.of_has_finite_products
 
 open category_theory
 open tactic
@@ -13,16 +14,9 @@ universes u v
 
 namespace category_theory.monoidal
 
-instance types : monoidal_category.{u+1} (Type u) :=
-{ tensor_obj := λ X Y, X × Y,
-  tensor_hom := λ _ _ _ _ f g, prod.map f g,
-  tensor_unit := punit,
-  left_unitor := λ X, (equiv.punit_prod X).to_iso,
-  right_unitor := λ X, (equiv.prod_punit X).to_iso,
-  associator := λ X Y Z, (equiv.prod_assoc X Y Z).to_iso,
-  ..category_theory.types.{u+1} }
+local attribute [instance] monoidal_of_has_finite_products
+instance types : monoidal_category.{u+1} (Type u) := by apply_instance
 
--- TODO Once we add braided/symmetric categories, include the braiding.
--- TODO More generally, define the symmetric monoidal structure on any category with products.
+-- TODO Once we add braided/symmetric categories, include the braiding/symmetry.
 
 end category_theory.monoidal