feat: port CategoryTheory.Limits.Creates (#2646)

leanprover-community · Mar 6, 2023 · de999b2 · de999b2
1 parent fa0f201
commit de999b2
Show file tree

Hide file tree

Showing 2 changed files with 680 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -288,6 +288,7 @@ import Mathlib.CategoryTheory.IsomorphismClasses
 import Mathlib.CategoryTheory.LiftingProperties.Adjunction
 import Mathlib.CategoryTheory.LiftingProperties.Basic
 import Mathlib.CategoryTheory.Limits.Cones
+import Mathlib.CategoryTheory.Limits.Creates
 import Mathlib.CategoryTheory.Limits.Filtered
 import Mathlib.CategoryTheory.Limits.FunctorCategory
 import Mathlib.CategoryTheory.Limits.HasLimits