[Merged by Bors] - chore(CategoryTheory/Limits/Shapes/BinaryProducts): More universe flexibility for pairComp
#17586
+2
−2
pairComp
#17586