chore: split Limits/Shapes/Terminal.lean to reduce imports (#18229)

The parts that require `HasLimit` stay in `Terminal.lean`, and the parts that only require `IsLimit` go to `IsTerminal.lean`. Found using the new `lake exe unused`. Co-authored-by: Markus Himmel <[email protected]>
leanprover-community · Oct 25, 2024 · aea6f29 · aea6f29
1 parent a4411e6
commit aea6f29
Show file tree

Hide file tree

Showing 11 changed files with 448 additions and 392 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1733,6 +1733,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
 import Mathlib.CategoryTheory.Limits.Shapes.FunctorCategory
 import Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
 import Mathlib.CategoryTheory.Limits.Shapes.Images
+import Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
 import Mathlib.CategoryTheory.Limits.Shapes.KernelPair
 import Mathlib.CategoryTheory.Limits.Shapes.Kernels
 import Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

diff --git a/Mathlib/CategoryTheory/Adjunction/Comma.lean b/Mathlib/CategoryTheory/Adjunction/Comma.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
+import Mathlib.CategoryTheory.Limits.Shapes.Terminal
 import Mathlib.CategoryTheory.Adjunction.Basic
 import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
 import Mathlib.CategoryTheory.PUnit

diff --git a/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean b/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Yuma Mizuno. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuma Mizuno
 -/
+import Mathlib.CategoryTheory.Limits.Shapes.Terminal
 import Mathlib.CategoryTheory.Bicategory.Kan.IsKan
 
 /-!

diff --git a/Mathlib/CategoryTheory/Comma/Over.lean b/Mathlib/CategoryTheory/Comma/Over.lean
@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Bhavik Mehta
 -/
 import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
-import Mathlib.CategoryTheory.PUnit
-import Mathlib.CategoryTheory.Functor.ReflectsIso
-import Mathlib.CategoryTheory.Functor.EpiMono
+import Mathlib.CategoryTheory.Category.Cat
 
 /-!
 # Over and under categories

diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
@@ -5,7 +5,7 @@ Authors: Adam Topaz, Kim Morrison
 -/
 import Mathlib.CategoryTheory.Comma.Basic
 import Mathlib.CategoryTheory.PUnit
-import Mathlib.CategoryTheory.Limits.Shapes.Terminal
+import Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
 
 /-!
 # The category of "structured arrows"

diff --git a/Mathlib/CategoryTheory/Elements.lean b/Mathlib/CategoryTheory/Elements.lean
@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
-import Mathlib.CategoryTheory.Groupoid
-import Mathlib.CategoryTheory.PUnit
+import Mathlib.CategoryTheory.Category.Cat
 
 /-!
 # The category of elements

diff --git a/Mathlib/CategoryTheory/Endofunctor/Algebra.lean b/Mathlib/CategoryTheory/Endofunctor/Algebra.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Joseph Hua. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Bhavik Mehta, Johan Commelin, Reid Barton, Robert Y. Lewis, Joseph Hua
 -/
-import Mathlib.CategoryTheory.Limits.Shapes.Terminal
+import Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
 
 /-!