diff --git a/src/category_theory/category/Cat.lean b/src/category_theory/category/Cat.lean
index 96cb69c50b1cb..cb487d840051b 100644
--- a/src/category_theory/category/Cat.lean
+++ b/src/category_theory/category/Cat.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import category_theory.concrete_category
+import category_theory.eq_to_hom
 
 /-!
 # Category of categories
@@ -29,15 +30,19 @@ namespace Cat
 
 instance : inhabited Cat := ⟨⟨Type u, category_theory.types⟩⟩
 
-instance str (C : Cat.{v u}) : category.{v u} C.α := C.str
+instance : has_coe_to_sort Cat :=
+{ S := Type u,
+  coe := bundled.α }
+
+instance str (C : Cat.{v u}) : category.{v u} C := C.str
 
 /-- Construct a bundled `Cat` from the underlying type and the typeclass. -/
 def of (C : Type u) [category.{v} C] : Cat.{v u} := bundled.of C
 
 /-- Category structure on `Cat` -/
 instance category : large_category.{max v u} Cat.{v u} :=
-{ hom := λ C D, C.α ⥤ D.α,
-  id := λ C, 𝟭 C.α,
+{ hom := λ C D, C ⥤ D,
+  id := λ C, 𝟭 C,
   comp := λ C D E F G, F ⋙ G,
   id_comp' := λ C D F, by cases F; refl,
   comp_id' := λ C D F, by cases F; refl,
@@ -46,9 +51,16 @@ instance category : large_category.{max v u} Cat.{v u} :=
 /-- Functor that gets the set of objects of a category. It is not
 called `forget`, because it is not a faithful functor. -/
 def objects : Cat.{v u} ⥤ Type u :=
-{ obj := bundled.α,
+{ obj := λ C, C,
   map := λ C D F, F.obj }
 
+/-- Any isomorphism in `Cat` induces an equivalence of the underlying categories. -/
+def equiv_of_iso {C D : Cat} (γ : C ≅ D) : C ≌ D :=
+{ functor := γ.hom,
+  inverse := γ.inv,
+  unit_iso := eq_to_iso $ eq.symm γ.hom_inv_id,
+  counit_iso := eq_to_iso γ.inv_hom_id }
+
 end Cat
 
 end category_theory
diff --git a/src/category_theory/functor_category.lean b/src/category_theory/functor_category.lean
index 2cec3e18b0d33..b32ad84014db5 100644
--- a/src/category_theory/functor_category.lean
+++ b/src/category_theory/functor_category.lean
@@ -65,6 +65,11 @@ infix ` ◫ `:80 := hcomp
 @[simp] lemma hcomp_app {H I : D ⥤ E} (α : F ⟶ G) (β : H ⟶ I) (X : C) :
   (α ◫ β).app X = (β.app (F.obj X)) ≫ (I.map (α.app X)) := rfl
 
+@[simp] lemma hcomp_id_app {H : D ⥤ E} (α : F ⟶ G) (X : C) : (α ◫ 𝟙 H).app X = H.map (α.app X) :=
+  by {dsimp, simp} -- See note [dsimp, simp].
+
+lemma id_hcomp_app {H : E ⥤ C} (α : F ⟶ G) (X : E) : (𝟙 H ◫ α).app X = α.app _ := by simp
+
 -- Note that we don't yet prove a `hcomp_assoc` lemma here: even stating it is painful, because we
 -- need to use associativity of functor composition. (It's true without the explicit associator,
 -- because functor composition is definitionally associative, but relying on the definitional equality
diff --git a/src/category_theory/monad/basic.lean b/src/category_theory/monad/basic.lean
index 0f5c9b32929b3..f17896aa6826b 100644
--- a/src/category_theory/monad/basic.lean
+++ b/src/category_theory/monad/basic.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison, Bhavik Mehta
+Authors: Scott Morrison, Bhavik Mehta, Adam Topaz
 -/
 import category_theory.functor_category
 
@@ -56,4 +56,90 @@ attribute [simp] comonad.left_counit comonad.right_counit
 notation `ε_` := comonad.ε
 notation `δ_` := comonad.δ
 
+/-- A morphisms of monads is a natural transformation compatible with η and μ. -/
+structure monad_hom (M N : C ⥤ C) [monad M] [monad N] extends nat_trans M N :=
+(app_η' : ∀ {X}, (η_ M).app X ≫ app X = (η_ N).app X . obviously)
+(app_μ' : ∀ {X}, (μ_ M).app X ≫ app X = (M.map (app X) ≫ app (N.obj X)) ≫ (μ_ N).app X . obviously)
+
+restate_axiom monad_hom.app_η'
+restate_axiom monad_hom.app_μ'
+attribute [simp, reassoc] monad_hom.app_η monad_hom.app_μ
+
+/-- A morphisms of comonads is a natural transformation compatible with η and μ. -/
+structure comonad_hom (M N : C ⥤ C) [comonad M] [comonad N] extends nat_trans M N :=
+(app_ε' : ∀ {X}, app X ≫ (ε_ N).app X = (ε_ M).app X . obviously)
+(app_δ' : ∀ {X}, app X ≫ (δ_ N).app X = (δ_ M).app X ≫ app (M.obj X) ≫ N.map (app X) . obviously)
+
+restate_axiom comonad_hom.app_ε'
+restate_axiom comonad_hom.app_δ'
+attribute [simp, reassoc] comonad_hom.app_ε comonad_hom.app_δ
+
+namespace monad_hom
+variables {M N L K : C ⥤ C} [monad M] [monad N] [monad L] [monad K]
+
+@[ext]
+theorem ext (f g : monad_hom M N) :
+  f.to_nat_trans = g.to_nat_trans → f = g := by {cases f, cases g, simp}
+
+variable (M)
+/-- The identity natural transformations is a morphism of monads. -/
+def id : monad_hom M M := { ..𝟙 M }
+variable {M}
+
+instance : inhabited (monad_hom M M) := ⟨id _⟩
+
+/-- The composition of two morphisms of monads. -/
+def comp (f : monad_hom M N) (g : monad_hom N L) : monad_hom M L :=
+{ app := λ X, f.app X ≫ g.app X }
+
+@[simp] lemma id_comp (f : monad_hom M N) : (monad_hom.id M).comp f = f :=
+by {ext, apply id_comp}
+@[simp] lemma comp_id (f : monad_hom M N) : f.comp (monad_hom.id N) = f :=
+by {ext, apply comp_id}
+/-- Note: `category_theory.monad.bundled` provides a category instance for bundled monads.-/
+@[simp] lemma assoc (f : monad_hom M N) (g : monad_hom N L) (h : monad_hom L K) :
+  (f.comp g).comp h = f.comp (g.comp h) := by {ext, apply assoc}
+
+end monad_hom
+
+namespace comonad_hom
+variables {M N L K : C ⥤ C} [comonad M] [comonad N] [comonad L] [comonad K]
+
+@[ext]
+theorem ext (f g : comonad_hom M N) :
+  f.to_nat_trans = g.to_nat_trans → f = g := by {cases f, cases g, simp}
+
+variable (M)
+/-- The identity natural transformations is a morphism of comonads. -/
+def id : comonad_hom M M := { ..𝟙 M }
+variable {M}
+
+instance : inhabited (comonad_hom M M) := ⟨id _⟩
+
+/-- The composition of two morphisms of comonads. -/
+def comp (f : comonad_hom M N) (g : comonad_hom N L) : comonad_hom M L :=
+{ app := λ X, f.app X ≫ g.app X }
+
+@[simp] lemma id_comp (f : comonad_hom M N) : (comonad_hom.id M).comp f = f :=
+by {ext, apply id_comp}
+@[simp] lemma comp_id (f : comonad_hom M N) : f.comp (comonad_hom.id N) = f :=
+by {ext, apply comp_id}
+/-- Note: `category_theory.monad.bundled` provides a category instance for bundled comonads.-/
+@[simp] lemma assoc (f : comonad_hom M N) (g : comonad_hom N L) (h : comonad_hom L K) :
+  (f.comp g).comp h = f.comp (g.comp h) := by {ext, apply assoc}
+
+end comonad_hom
+
+namespace monad
+instance : monad (𝟭 C) :=
+{ η := 𝟙 _,
+  μ := 𝟙 _ }
+end monad
+
+namespace comonad
+instance : comonad (𝟭 C) :=
+{ ε := 𝟙 _,
+  δ := 𝟙_ }
+end comonad
+
 end category_theory
diff --git a/src/category_theory/monad/bundled.lean b/src/category_theory/monad/bundled.lean
new file mode 100644
index 0000000000000..e11f5261cb08e
--- /dev/null
+++ b/src/category_theory/monad/bundled.lean
@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2020 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz
+-/
+import category_theory.monad.basic
+import category_theory.eq_to_hom
+
+/-!
+# Bundled Monads
+
+We define bundled (co)monads as a structure consisting of a functor `func : C ⥤ C` endowed with
+a term of type `(co)monad func`. See `category_theory.monad.basic` for the definition.
+The type of bundled (co)monads on a category `C` is denoted `(Co)Monad C`.
+
+We also define morphisms of bundled (co)monads as morphisms of their underlying (co)monads
+in the sense of `category_theory.(co)monad_hom`. We construct a category instance on `(Co)Monad C`.
+-/
+
+namespace category_theory
+open category
+
+universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+
+variables (C : Type u) [category.{v} C]
+
+/-- Bundled monads. -/
+structure Monad :=
+(func : C ⥤ C)
+(str : monad func . tactic.apply_instance)
+
+/-- Bundled comonads -/
+structure Comonad :=
+(func : C ⥤ C)
+(str : comonad func . tactic.apply_instance)
+
+namespace Monad
+
+/-- The initial monad. TODO: Prove it's initial. -/
+def initial : Monad C := { func := 𝟭 _ }
+
+variable {C}
+
+instance : inhabited (Monad C) := ⟨initial C⟩
+
+instance {M : Monad C} : monad M.func := M.str
+
+/-- Morphisms of bundled monads. -/
+def hom (M N : Monad C) := monad_hom M.func N.func
+
+namespace hom
+instance {M : Monad C} : inhabited (hom M M) := ⟨monad_hom.id _⟩
+end hom
+
+instance : category (Monad C) :=
+{ hom := hom,
+  id := λ _, monad_hom.id _,
+  comp := λ _ _ _, monad_hom.comp }
+
+/-- The forgetful functor from `Monad C` to `C ⥤ C`. -/
+def forget : Monad C ⥤ (C ⥤ C) :=
+{ obj := func,
+  map := λ _ _ f, f.to_nat_trans }
+
+@[simp]
+lemma comp_to_nat_trans {M N L : Monad C} (f : M ⟶ N) (g : N ⟶ L) :
+  (f ≫ g).to_nat_trans = nat_trans.vcomp f.to_nat_trans g.to_nat_trans := rfl
+
+@[simp] lemma assoc_func_app {M : Monad C} {X : C} :
+  M.func.map ((μ_ M.func).app X) ≫ (μ_ M.func).app X =
+  (μ_ M.func).app (M.func.obj X) ≫ (μ_ M.func).app X := by apply monad.assoc
+
+end Monad
+
+namespace Comonad
+
+/-- The terminal comonad. TODO: Prove it's terminal. -/
+def terminal : Comonad C := { func := 𝟭 _ }
+
+variable {C}
+
+instance : inhabited (Comonad C) := ⟨terminal C⟩
+
+instance {M : Comonad C} : comonad M.func := M.str
+
+/-- Morphisms of bundled comonads. -/
+def hom (M N : Comonad C) := comonad_hom M.func N.func
+
+namespace hom
+instance {M : Comonad C} : inhabited (hom M M) := ⟨comonad_hom.id _⟩
+end hom
+
+instance : category (Comonad C) :=
+{ hom := hom,
+  id := λ _, comonad_hom.id _,
+  comp := λ _ _ _, comonad_hom.comp }
+
+/-- The forgetful functor from `CoMonad C` to `C ⥤ C`. -/
+def forget : Comonad C ⥤ (C ⥤ C) :=
+{ obj := func,
+  map := λ _ _ f, f.to_nat_trans }
+
+@[simp]
+lemma comp_to_nat_trans {M N L : Comonad C} (f : M ⟶ N) (g : N ⟶ L) :
+  (f ≫ g).to_nat_trans = nat_trans.vcomp f.to_nat_trans g.to_nat_trans := rfl
+
+@[simp] lemma coassoc_func_app {M : Comonad C} {X : C} :
+  (δ_ M.func).app X ≫ M.func.map ((δ_ M.func).app X) =
+  (δ_ M.func).app X ≫ (δ_ M.func).app (M.func.obj X) := by apply comonad.coassoc
+
+end Comonad
+end category_theory
diff --git a/src/category_theory/monad/equiv_mon.lean b/src/category_theory/monad/equiv_mon.lean
new file mode 100644
index 0000000000000..267f30b02f34f
--- /dev/null
+++ b/src/category_theory/monad/equiv_mon.lean
@@ -0,0 +1,117 @@
+/-
+Copyright (c) 2020 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz
+-/
+import category_theory.monad.bundled
+import category_theory.monoidal.End
+import category_theory.monoidal.internal
+import category_theory.category.Cat
+
+/-!
+
+# The equivalence between `Monad C` and `Mon_ (C ⥤ C)`.
+
+A monad "is just" a monoid in the category of endofunctors.
+
+# Definitions/Theorems
+
+1. `to_Mon` associates a monoid object in `C ⥤ C` to any monad on `C`.
+2. `Monad_to_Mon` is the functorial version of `to_Mon`.
+3. `of_Mon` associates a monad on `C` to any monoid object in `C ⥤ C`.
+4. `Monad_Mon_equiv` is the equivalence between `Monad C` and `Mon_ (C ⥤ C)`.
+
+-/
+
+namespace category_theory
+open category
+
+universes v u -- declare the `v`'s first; see `category_theory.category` for an explanation
+variables {C : Type u} [category.{v} C]
+
+namespace Monad
+local attribute [instance, reducible] endofunctor_monoidal_category
+
+/-- To every `Monad C` we associated a monoid object in `C ⥤ C`.-/
+@[simps]
+def to_Mon : Monad C → Mon_ (C ⥤ C) := λ M,
+{ X := M.func,
+  one := η_ _,
+  mul := μ_ _ }
+
+variable (C)
+/-- Passing from `Monad C` to `Mon_ (C ⥤ C)` is functorial. -/
+@[simps]
+def Monad_to_Mon : Monad C ⥤ Mon_ (C ⥤ C) :=
+{ obj := to_Mon,
+  map := λ _ _ f, { hom := f.to_nat_trans } }
+variable {C}
+
+/-- To every monoid object in `C ⥤ C` we associate a `Monad C`. -/
+@[simps]
+def of_Mon : Mon_ (C ⥤ C) → Monad C := λ M,
+{ func := M.X,
+  str :=
+  { η := M.one,
+    μ := M.mul,
+    assoc' := begin
+      intro X,
+      rw [←nat_trans.hcomp_id_app, ←nat_trans.comp_app],
+      simp,
+    end,
+    left_unit' := begin
+      intro X,
+      rw [←nat_trans.id_hcomp_app, ←nat_trans.comp_app, M.mul_one],
+      refl,
+    end,
+    right_unit' := begin
+      intro X,
+      rw [←nat_trans.hcomp_id_app, ←nat_trans.comp_app, M.one_mul],
+      refl,
+    end } }
+
+variable (C)
+/-- Passing from `Mon_ (C ⥤ C)` to `Monad C` is functorial. -/
+@[simps]
+def Mon_to_Monad : Mon_ (C ⥤ C) ⥤ Monad C :=
+{ obj := of_Mon,
+  map := λ _ _ f,
+  { app_η' := begin
+      intro X,
+      erw [←nat_trans.comp_app, f.one_hom],
+      refl,
+    end,
+    app_μ' := begin
+      intro X,
+      erw [←nat_trans.comp_app, f.mul_hom],
+      finish,
+    end,
+    ..f.hom } }
+variable {C}
+
+/-- Isomorphism of functors used in `Monad_Mon_equiv` -/
+@[simps]
+def of_to_mon_end_iso : Mon_to_Monad C ⋙ Monad_to_Mon C ≅ 𝟭 _ :=
+{ hom := { app := λ _, { hom := 𝟙 _ } },
+  inv := { app := λ _, { hom := 𝟙 _ } } }
+
+/-- Isomorphism of functors used in `Monad_Mon_equiv` -/
+@[simps]
+def to_of_mon_end_iso : Monad_to_Mon C ⋙ Mon_to_Monad C ≅ 𝟭 _ :=
+{ hom := { app := λ _, { app := λ _, 𝟙 _ } },
+  inv := { app := λ _, { app := λ _, 𝟙 _ } } }
+
+variable (C)
+/-- Oh, monads are just monoids in the category of endofunctors (equivalence of categories). -/
+@[simps]
+def Monad_Mon_equiv : (Monad C) ≌ (Mon_ (C ⥤ C)) :=
+{ functor := Monad_to_Mon _,
+  inverse := Mon_to_Monad _,
+  unit_iso := to_of_mon_end_iso.symm,
+  counit_iso := of_to_mon_end_iso }
+
+-- Sanity check
+example (A : Monad C) {X : C} : ((Monad_Mon_equiv C).unit_iso.app A).hom.app X = 𝟙 _ := rfl
+
+end Monad
+end category_theory