Commit 2026-06-24 10:57 3b0b30fd
View on Github →chore(CategoryTheory/EqToHom): use to_dual none (#40965)
This PR tags eqToHom with to_dual. Unfortunately ,eqToHom is not conveniently self dual, because for this the direction of the equality needs to be swapped. So, we mostly use to_dual none to generate non-user-facing duals. This is needed to dualize some proofs later on.