Remove Categories.Category.Equivalence

[iwilare]

We were working on something that often requires isomorphism reasoning on categories (and, by extension, domains and codomains of functors).

Currently, there are two different versions of equivalence of Categories that can be conjured up.

• One defined in Categories.Category.Equivalence, with two functors and weak-inverse as proof
• The other possibility is opening Morphism.Reasoning.Iso instantiated on Cats.

This evidently creates problems, as one cannot use any kind of object isomorphism reasoning when using StrongEquivalence, and, viceversa, one cannot reason on particular properties of categories when Iso is used (e.g., op preserves isos). It would be desirable for it to only exist one "correct" way of doing things, so that existing/more general tools (such as some kind of general isomorphism reasoning on objects) can be used.

We propose the following as solution to these issues:

• remove the definition of StrongEquivalence in favour of opening Iso with Cats;
• refactor all current usages of StrongEquivalence to use Iso; (should be somewhat of a mechanical job)
• adapt current Category-specific notions of equivalence to use Iso.

(Another useful step would be separating Morphism.Reasoning from Morphism.Reasoning.Iso: one refers to morphisms, the other one refers to objects. Something like Object.Reasoning.Iso?)

[JacquesCarette]

Doing this in small steps makes sense. Starting with Object.Reasoning.Iso seems like a good idea. Regarding the 3 steps of your proposed solution, I would think that doing them exactly backwards (i.e. first adapt the notions, then refactor away, then finally remove the definition of StrongEquivalence) will likely work best. Each small step is a valid refactor on its own.