diff --git a/Mathlib/CategoryTheory/Limits/IsConnected.lean b/Mathlib/CategoryTheory/Limits/IsConnected.lean
index 0992ce259bd2e..200ed0d40bc86 100644
--- a/Mathlib/CategoryTheory/Limits/IsConnected.lean
+++ b/Mathlib/CategoryTheory/Limits/IsConnected.lean
@@ -39,7 +39,9 @@ unit-valued, singleton, colimit
 
 universe w v u
 
-namespace CategoryTheory.Limits.Types
+namespace CategoryTheory
+
+namespace Limits.Types
 
 variable (C : Type u) [Category.{v} C]
 
@@ -111,8 +113,15 @@ theorem isConnected_iff_isColimit_pUnitCocone :
   simp only [isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{w} C]
   exact ⟨colimit.isoColimitCocone colimitCocone⟩
 
+end Limits.Types
+
+namespace Functor
+
+open Limits.Types
+
 universe v₂ u₂
-variable {C : Type u} {D : Type u₂} [Category.{v} C] [Category.{v₂} D]
+
+variable {C : Type u} [Category.{v} C] {D : Type u₂} [Category.{v₂} D]
 
 /-- The domain of a final functor is connected if and only if its codomain is connected. -/
 theorem isConnected_iff_of_final (F : C ⥤ D) [F.Final] : IsConnected C ↔ IsConnected D := by
@@ -126,4 +135,6 @@ theorem isConnected_iff_of_initial (F : C ⥤ D) [F.Initial] : IsConnected C ↔
   rw [isConnected_iff_isConnected_op C, isConnected_iff_isConnected_op D]
   exact isConnected_iff_of_final F.op
 
-end CategoryTheory.Limits.Types
+end Functor
+
+end CategoryTheory