chore(CategoryTheory/Limits/Shapes/BinaryProducts): More universe fle…

…xibility for `pairComp` (#17586)

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) :=