Equivalences of wild categories

[ThomatoTomato]

It doesn't look like the library has a notion of equivalences between wild categories. I might have just been looking in the wrong places, so please feel free to correct me on this. However, if one were to define this, what would the best approach be?

For wild 1-categoriese I would hope that an equivalence would be an essentially surjective and fully faithfull functor. Is this the way we would want to implement this, or is there another way that's better? I see for instance that split essentially surjective is used in EquivGpd.v. Is this extra constructive data necessary for our definition of equivalences?

There is for instance a notion of equivalences within wild categories. Could an approach to this be to define a wild category of U-small wild categories, and then recover the notion of equivalence through this?

[jdchristensen]

And a related question is whether @Alizter or @mikeshulman know of any existing formalization of this that could be used.

[mikeshulman]

There may be more than one notion of equivalence that are useful for different purposes. However, my guess would be that the split essentially surjective version is more useful, and that there's at least one way of defining a wild category of wild categories so that those are the equivalences you get out. I don't recall specifically a formalization of this.

[Alizter]

The obvious notion of equivalence you get from the quasi-invertible functors is a little redundant. I think it suffices for CatEquiv A B to be (morally) {f : Fun11 A B & IsEquiv F}. The functoriality of the inverse should be provable. Then CatIsEquiv is just IsEquiv for the underlying map of a functor. This should mean it is equivalent to the quasi-invertible definition.

There are other notions of equivalences that people have studied. I think the one Mike wrote down in #1302 is similar to the coinductive approach detailed in https://arxiv.org/pdf/2008.10307. I believe I have seen others experiment with similar ideas before. I don't think this would be the right direction as it broadens the scope of exploration more so than is necessary.

With regards to the fully faithful + split essentially surjective question, formalisations in the 1lab exist https://1lab.dev/Cat.Functor.Equivalence.html which you could probably reproduce without too much trouble. Something useful to show would be that we have an adjunct pair from any equivalence.

In any case, you will need to introduce a type of bundled category. Morally OneCat := {A : Type & Is1Cat A}. This will probably be better as a record as you need other fields too. Then you would show that this is a TwoOneCat. I don't see any reason to introduce bicategories just yet, so (2,1)-categories should suffice.

[jdchristensen]

CatIsEquiv is just IsEquiv for the underlying map of a functor.

I don't think that makes sense for non-univalent categories. It uses the paths in the types of objects rather than the specified 1-cells. For example, with that definition, any functor A -> B would be an equivalence when A and B have Unit as their type of objects. (Think of BG, for example.)

There are other notions of equivalences that people have studied. I think the one Mike wrote down in #1302 is similar to the coinductive approach detailed in https://arxiv.org/pdf/2008.10307.

For others, here's the spot in #1302 that defines equivalences: https://github.com/HoTT/Coq-HoTT/pull/1302/files#diff-e53797b6f41210c5b77e8042e7e56fb4854cc055ebbdd264f026066305cb53ba

However, it's not clear to me how high we need to go in the recursion.

In any case, you will need to introduce a type of bundled category.

This is needed only if we write down a wild-category of wild-categories. But I think that for the short term, it would be fine to just define what it means for a functor between wild-categories to be an equivalence, and work with that notion.