mathlib3

d69501f1 - feat(category_theory/limits/shapes/multiequalizer): Multi(co)equalizers (#10169)

feat(category_theory/limits/shapes/multiequalizer): Multi(co)equalizers (#10169) This PR adds another special shape to the limits library, which directly generalizes shapes for many other special limits (like pullbacks, equalizers, etc.). A `multiequalizer` can be thought of an an equalizer of two maps between two products. This will be used later on in the context of sheafification. I don't know if there is a standard name for the gadgets this PR introduces. I would be happy to change the names if needed.