Commit 2024-02-07 10:11 3eb9163a

refactor: move natural isomorphisms involving inverses of equivalences (#10278)

• Move all results from CategoryTheory/Functor/InvIsos.lean to CategoryTheory/Equivalence.lean and delete the former file
• Replace use of eqToIso (Functor.comp_id G) with G.rightUnitor
• Move into Iso namespace to enable dot notation
• Add analogous results stated in terms of Equivalence instead of IsEquivalence