search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

Equivalences of wild categories #2128

Open ThomatoTomato opened 2 hours ago

ThomatoTomato commented 2 hours ago

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 commented 2 hours ago

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

mikeshulman commented 1 hour ago

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.