feat: port CategoryTheory.Monoidal.Category (#2318)

leanprover-community · Feb 18, 2023 · ec01d38 · ec01d38
1 parent 828f88f
commit ec01d38
Show file tree

Hide file tree

Showing 2 changed files with 734 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -248,6 +248,7 @@ import Mathlib.CategoryTheory.Functor.InvIsos
 import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Groupoid.Basic
 import Mathlib.CategoryTheory.Iso
+import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Opposites