Commit 2025-06-15 11:36 d6898ad6

View on Github →

refactor(RelCat): use a type synonym for homs (#25593) This improves automation and follows the new pattern for concrete categories (although RelCat is not a concrete category).

Estimated changes

Modified Mathlib/CategoryTheory/Category/RelCat.lean

added theorem CategoryTheory.RelCat.Hom.ext

modified theorem CategoryTheory.RelCat.Hom.rel_comp_apply₂

modified theorem CategoryTheory.RelCat.Hom.rel_id_apply₂

added structure CategoryTheory.RelCat.Hom

modified theorem CategoryTheory.RelCat.graphFunctor_map

deleted theorem CategoryTheory.RelCat.hom_ext

modified def CategoryTheory.RelCat.opEquivalence