Commit 2024-07-19 10:46 4c31303a
View on Github →feat(Bicategory/NaturalTransformation/Strong): define strong natural transformations (#14028)
We define strong natural transformations of oplax functors, and provide API for going between strong and oplax natural transformations. We also move & rename the file NaturalTransformation.lean, which defines oplax natural transformations, to NaturalTransformation/Oplax.lean. This should make it easier to also add lax natural transformations in the future.