Commit 2025-08-23 07:32 34519ccd
View on Github →chore(CategoryTheory): process some porting notes (#28741)
This PR goes alphabetically through all porting notes for category theory up to (but excluding for the most part) CategoryTheory/Limits and fixes the ones that have an obvious resolution. Some of them are won'tfixes or TODOs unrelated to the port.