Commit 2024-05-08 11:06 2113c23b

refactor(CategoryTheory): make Functor.IsEquivalence a Prop (#12462) Functor.IsEquivalence is now the combination of F.Full, F.Faithful and F.EssSurj. That such a functor is an equivalence (i.e. there is a quasi-inverse, etc.) is now contained in the definition F.asEquivalence. This refactor is to avoid any diamond in the IsEquivalence instances (and also for IsLeftAdjoint and IsRightAdjoint which are also made Props). If data is important, one should use Equivalence or Adjunction instead. This refactor also avoids some duplication of code between the structures Equivalence and the former IsEquivalence. IsLeftAdjoint and IsRightAdjoint are moved to the Functor namespace. The namespaces have also been fixed in the file CategoryTheory.Adjunction.FullyFaithful. Proofs have been tidied in CategoryTheory.Monoidal.NaturalTransformation. Definitions which relied on IsLeft/RightAdjoint have been modified in order to contain the data of an adjunction (e.g. Reflective, MonadicRightAdjoint, etc.).