From 7817d20eb8249e7a5acd2eef4e046b37407b7f2c Mon Sep 17 00:00:00 2001
From: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
Date: Wed, 9 Oct 2024 15:32:15 +0000
Subject: [PATCH] chore(CategoryTheory/Limits/Shapes/BinaryProducts): More
 universe flexibility for `pairComp` (#17586)

---
 Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
index 4ea865a6b1d0d..351236724ffa1 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
@@ -31,7 +31,7 @@ braiding and associating isomorphisms, and the product comparison morphism.
 
 noncomputable section
 
-universe v u u₂
+universe v v₁ u u₁ u₂
 
 open CategoryTheory
 
@@ -160,7 +160,7 @@ def diagramIsoPair (F : Discrete WalkingPair ⥤ C) :
 
 section
 
-variable {D : Type u} [Category.{v} D]
+variable {D : Type u₁} [Category.{v₁} D]
 
 /-- The natural isomorphism between `pair X Y ⋙ F` and `pair (F.obj X) (F.obj Y)`. -/
 def pairComp (X Y : C) (F : C ⥤ D) : pair X Y ⋙ F ≅ pair (F.obj X) (F.obj Y) :=