Commit 2025-09-17 09:25 8afdc2e5
View on Github →chore: rename hom_to_functor, id_to_functor (#29250)
The files CategoryTheory.Category.Grpd and CategoryTheory.Category.Cat should be consistent in naming conventions and style. Here I renamed CategoryTheory.Grpd.hom_to_functor to CategoryTheory.Grpd.comp_eq_comp to mirror CategoryTheory.Cat.comp_eq_comp. Similarly I renamed CategoryTheory.Grpd.id_to_functor to CategoryTheory.Grpd.id_eq_eq