Commit 2025-08-27 19:15 71e57acb
View on Github →chore(CategoryTheory): process remaining porting notes for CategoryTheory (#28782)
Thiis should cover all the remaining easy to deal with porting notes for CategoryTheory. Most of those that were not easily fixed are about Lean 4 being stricter about defeq, which is not going to change.
The most important sources of remaining porting notes in CategoryTheory are ext
not firing (due to defeq issues), and congr
not firing (due to reasons I don't know).