Commit 2026-01-16 12:21 cdb6f72a
View on Github →feat(CategoryTheory/NatTrans): use to_dual (#33834)
This PR tags NatTrans with to_dual. The two functor arguments get swapped because the underlying NatTrans.app has its direction swapped.
Translating the naturality field is slightly awkward. We need to define a constant naturality' (analogously to `Category.assoc')