Commit 2024-09-27 01:46 652e6e77
View on Github →refactor(Algebra/Category/ModuleCat): redefine presheaves of modules as families of objects in ModuleCat (#16667)
In order to ease automation, a presheaf of modules is redefined as a family of objects in ModuleCat. Previously, it was defined as a presheaf of abelian groups with extra data, which was eventually creating a lot of issues with automation.