Commit 2026-06-22 18:03 f07d1202
View on Github →chore(CategoryTheory/Comma/Arrow): use to_dual (#40862)
This PR uses to_dual to dualize the Arrow category.
Theorems isIso_of_isIso and isIso_of_isIso' did not have a dual, and had stronger iff forms, and weren't used, so I decided to remove them (or mark private).
I skipped the parts involving eqToHom, since eqToHom hasn't been tagged with to_dual yet.