Commit 2025-04-27 18:32 04fc112d
View on Github →feat(CategoryTheory): the center of a category (#23777)
This PR introduces an abbrevation CatCenter C for the center of a category C, i.e. the type of endomorphisms of the identity functor of C.