Commit 2025-05-20 14:06 0411276d

feat(CategoryTheory/Equivalence): functoriality of symmetry of equivalences (#23198) We introduce a file CategoryTheory/Equivalence/Symmetry in which we continue to provide basic API for the category structure on equivalences defined in #23197. We prove that symmetry of equivalences defines an equivalence (C ≌ D) ≌ (D ≌ C)ᵒᵖ, and we use this to construct Equivalence.inverseFunctor: (C ≌ D) ⥤ (D ⥤ C)ᵒᵖ that takes an equivalence to its inverse functor, and to promote Equivalence.congrLeft to a functor.