Commit 2025-11-28 10:31 eeda3205
View on Github →feat(Bicategory/Modification/Pseudo): define modifications between strong natural transformations of pseudofunctors (#30895) This PR adds modifications between strong natural transformations of pseudofunctors. At the same time, it improves the existing code on modifications between oplax natural tranformations of oplax functors (by removing some simp lemmas). This is a migration of #18254 to a fork.