chore(category_theory/monads): remove empty file (#6915)

In #5889 I moved the contents of this file into monad/basic but I forgot to delete this file.
leanprover-community · Mar 27, 2021 · 06b21d0 · 06b21d0
1 parent 27c8676
commit 06b21d0
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 28 deletions.
diff --git a/src/category_theory/monad/bundled.lean b/src/category_theory/monad/bundled.lean
diff --git a/src/category_theory/monad/equiv_mon.lean b/src/category_theory/monad/equiv_mon.lean
@@ -3,7 +3,7 @@ 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.monad.basic
 import category_theory.monoidal.End
 import category_theory.monoidal.Mon_
 import category_theory.category.Cat