Messed up vars order...

leanprover-community · Feb 25, 2025 · 3397ed2 · 3397ed2
1 parent 90c6369
commit 3397ed2
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/Mathlib/CategoryTheory/Sums/Basic.lean b/Mathlib/CategoryTheory/Sums/Basic.lean
@@ -148,8 +148,10 @@ end Swap
 
 end Sum
 
-variable {A : Type u₁} [Category.{v₁} A] {B : Type u₂} [Category.{v₂} B] {C : Type u₁}
-  [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] {A' : Type u₁} [Category.{v₁} A']
+variable {A : Type u₁} [Category.{v₁} A] {A' : Type u₁} [Category.{v₁} A']
+  {B : Type u₂} [Category.{v₂} B]
+  {C : Type u₁} [Category.{v₁} C]
+  {D : Type u₂} [Category.{v₂} D]
 
 namespace Functor