Commit 2026-03-16 18:02 867c38ab
View on Github →feat(CategoryTheory/Equivalence): tag Equivalence with to_dual (#36579)
This PR tags Equivalence with to_dual. This will allow us to dualize equivalences with to_dual.
This PR also adds dsimp% in modified declarations, in order to get rid of some backward.isDefEq.respectTransparency.
It is quite annoying that we have to manually write out the dual of Equivalence.functor_unitIso_comp and Equivalence.mk'. Hopefully this can be done more automatically in the future.