Commit 2025-09-26 06:47 f636b7af
View on Github →chore(CategoryTheory/Sites): remove FamilyOfElements.compPresheafMap in favour of .map (#29977)
Remove FamilyOfElements.compPresheafMap in favour of FamilyOfElements.map, a definitionally equivalent declaration that has also been around for a while - see zulip. Since no one expressed any preference regarding which of the two definitions to keep I've just gone ahead and picked FamilyOfElements.compPresheafMap for removal here.