feat: port CategoryTheory.Bicategory.Basic (#2126)

Pretty straightforward except I don't know how to use aesop_cat in place of ext.
leanprover-community · Feb 7, 2023 · 8e132e2 · 8e132e2
1 parent e37d93e
commit 8e132e2
Show file tree

Hide file tree

Showing 3 changed files with 508 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -211,6 +211,7 @@ import Mathlib.Algebra.Support
 import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
+import Mathlib.CategoryTheory.Bicategory.Basic
 import Mathlib.CategoryTheory.Category.Basic
 import Mathlib.CategoryTheory.Category.KleisliCat
 import Mathlib.CategoryTheory.Category.RelCat