From 3397ed2f451086d2e996e428e4952151b7c6c26f Mon Sep 17 00:00:00 2001 From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> Date: Tue, 25 Feb 2025 13:14:36 +0100 Subject: [PATCH] Messed up vars order... --- Mathlib/CategoryTheory/Sums/Basic.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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