Commit 2024-12-03 14:22 ac7c96fc

chore(Algebra/Category/ModuleCat): rename ModuleCat.asHom to ModuleCat.ofHom (#19705) As discussed in the comments for #19511. It seems the choice between ofHom and asHom is somewhat inconsistent in concrete categories, but ofHom wins. In particular, we want to be consistent with the newly refactored AlgebraCat.ofHom and the constructor for objects ModuleCat.of. The choice between asHom and ofHom was only made a few months ago: #17476. It's a bit unfortunate to go back on something that was deprecated so recently, but I think the result is worth the pain. I have not touched asHomLeft and asHomRight since #19511 will replace these with ofHom everywhere anyway.