[Merged by Bors] - chore(CategoryTheory/Limits/Shapes/BinaryProducts): More universe flexibility for pairComp
#22778
Loading
pairComp
#22778