Commit 2025-04-15 16:43 b533ec6d

feat(CategoryTheory/Limits): multicoequalizers attached to linear orders (#22203) Certain multicoequalizers are defined by coequalizing maps V ⟨i, j⟩ ⟶ U i and V ⟨i, j⟩ ⟶ U j for i and j in a type ι. When ι is linearly ordered and if the objects V satisfy a certain symmetry, we show that it suffices to consider the "relations" given by tuples ⟨i, j⟩ such that i < j.