Commit 2025-05-12 14:24 555df869

feat(Bicategory/NaturalTransformation): strong transformations between pseudofunctors (#18253) This PR adds strong transformations between pseudofunctors. This is more or less a copy of my previous implementation of strong transformations between oplax functors, but I have added/improved the API a bit. Previously, one could talk about strong transformations between pseudofunctors by using strong transformations between the underlying oplax functors. However, since there should also be strong transformations between lax functors, this approach is somewhat unnatural and I think its better to define these directly in terms of pseudofunctors. This is used in an upcoming PR where I define the bicategory of pseudofunctors. Whilst doing this I have moved the old code for strong transformations between oplax functors to the file Oplax where oplax transformations between oplax functors has been defined. This should make the distinction less confusing. Note that there is not much content in this PR (despite the line count), it is mainly moving things around and copying code to an almost identical situation!