feat: port/CategoryTheory.Limits.FunctorCategory (#2380)

leanprover-community · Mar 2, 2023 · 2affd54 · 2affd54
1 parent 5d9a516
commit 2affd54
Show file tree

Hide file tree

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