diff --git a/Mathlib/CategoryTheory/Sums/Basic.lean b/Mathlib/CategoryTheory/Sums/Basic.lean index 4d054b25c363c..f134d08b311ba 100644 --- 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