Commit 2024-08-19 18:48 56b132b9

chore: remove unnecessary uses of CategoryTheory.Equivalence.mk (#15919) An equivalence of categories consists of a functor, an inverse, and unit and counit isomorphisms which satisfy the same compatibilities as for adjoint functors. However, certain equivalences are constructed via the constructor Equivalence.mk which does not assume these compatibilities: by changing the unit isomorphism, it is possible to satisfy the compatibility. When only the existence of an equivalence matters, we may certainly use Equivalence.mk (e.g. inside proofs). However, the more we develop the library, the more we may need to unfold the definitions of unit/counit isomorphisms (as it happened in #12728). Then, I would suggest that we refrain from using Equivalence.mk as much as possible. In this PR, most uses of Equivalence.mk are removed: in most cases, the compatibilities satisfied by adjunctions were easy to prove.