diff --git a/src/category/basic.lean b/src/category/basic.lean
index dfa2daf94f237..64bbb6dcfc114 100644
--- a/src/category/basic.lean
+++ b/src/category/basic.lean
@@ -138,6 +138,29 @@ def list.mmap_accuml (f : β' → α → m' (β' × γ')) : β' → list α →
 
 end monad
 
+section
+variables {m : Type u → Type u} [monad m] [is_lawful_monad m]
+
+lemma mjoin_map_map {α β : Type u} (f : α → β) (a : m (m α)) :
+  mjoin (functor.map f <$> a) = f <$> (mjoin a) :=
+by simp only [mjoin, (∘), id.def,
+  (bind_pure_comp_eq_map _ _ _).symm, bind_assoc, map_bind, pure_bind]
+
+lemma mjoin_map_mjoin {α : Type u} (a : m (m (m α))) :
+  mjoin (mjoin <$> a) = mjoin (mjoin a) :=
+by simp only [mjoin, (∘), id.def,
+  map_bind, (bind_pure_comp_eq_map _ _ _).symm, bind_assoc, pure_bind]
+
+@[simp] lemma mjoin_map_pure {α : Type u} (a : m α) :
+  mjoin (pure <$> a) = a :=
+by simp only [mjoin, (∘), id.def,
+  map_bind, (bind_pure_comp_eq_map _ _ _).symm, bind_assoc, pure_bind, bind_pure]
+
+@[simp] lemma mjoin_pure {α : Type u} (a : m α) : mjoin (pure a) = a :=
+is_lawful_monad.pure_bind a id
+
+end
+
 section alternative
 variables {F : Type → Type v} [alternative F]
 
diff --git a/src/category_theory/monad/default.lean b/src/category_theory/monad/default.lean
index 31a825e9d3a84..78b9c222ec50d 100644
--- a/src/category_theory/monad/default.lean
+++ b/src/category_theory/monad/default.lean
@@ -1 +1,3 @@
-import category_theory.monad.limits
+import
+  category_theory.monad.limits
+  category_theory.monad.types
diff --git a/src/category_theory/monad/types.lean b/src/category_theory/monad/types.lean
new file mode 100644
index 0000000000000..c7063af322bb0
--- /dev/null
+++ b/src/category_theory/monad/types.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2019 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+-/
+
+import category_theory.monad.basic
+import category_theory.types
+
+/-!
+
+# Convert from `monad` (i.e. Lean's `Type`-based monads) to `category_theory.monad`
+
+This allows us to use these monads in category theory.
+
+-/
+
+namespace category_theory
+
+section
+universes u
+
+variables (m : Type u → Type u) [_root_.monad m] [is_lawful_monad m]
+
+instance : monad (of_type_functor m) :=
+{ η           := ⟨@pure m _, assume α β f, (is_lawful_applicative.map_comp_pure m f).symm ⟩,
+  μ           := ⟨@mjoin m _, assume α β (f : α → β), funext $ assume a, mjoin_map_map f a ⟩,
+  assoc'      := assume α, funext $ assume a, mjoin_map_mjoin a,
+  left_unit'  := assume α, funext $ assume a, mjoin_pure a,
+  right_unit' := assume α, funext $ assume a, mjoin_map_pure a }
+
+end
+
+end category_theory
diff --git a/src/category_theory/types.lean b/src/category_theory/types.lean
index 032c2ed3ad1c1..55111d77ace5d 100644
--- a/src/category_theory/types.lean
+++ b/src/category_theory/types.lean
@@ -110,6 +110,28 @@ begin
     exact (congr_fun H₂ x : _) }
 end
 
+section
+
+/-- `of_type_functor m` converts from Lean's `Type`-based `category` to `category_theory`. This
+allows us to use these functors in category theory. -/
+def of_type_functor (m : Type u → Type v) [_root_.functor m] [is_lawful_functor m] :
+  Type u ⥤ Type v :=
+{ obj       := m,
+  map       := λα β, _root_.functor.map,
+  map_id'   := assume α, _root_.functor.map_id,
+  map_comp' := assume α β γ f g, funext $ assume a, is_lawful_functor.comp_map f g _ }
+
+variables (m : Type u → Type v) [_root_.functor m] [is_lawful_functor m]
+
+@[simp]
+lemma of_type_functor_obj : (of_type_functor m).obj = m := rfl
+
+@[simp]
+lemma of_type_functor_map {α β} (f : α → β) :
+  (of_type_functor m).map f = (_root_.functor.map f : m α → m β) := rfl
+
+end
+
 end category_theory
 
 -- Isomorphisms in Type and equivalences.