Commit 2026-06-02 18:08 324e1c06

feat(CategoryTheory): define internal equivalence relations (#36541) Define internal equivalence relations in any category C, as a structure on parallel pairs of morphisms. Prove that equivalence relations on types are equivalence relations in the category of types. Prove that kernel pairs are equivalence relations. Define (universally) effective equivalence relations, and a associated class for categories in which every equivalence relation is effective universal. Prove that an effective equivalence relation yields a coequalizer diagram, and that the associated projection on the "quotient" of the relation is a regular epimorphism.