Removing truncation from the categories library

[Alizter]

How much of the categories library works when truncation is removed from the definition of category?

The reason I ask is because I would like to use some of this category theory, but I can't since everything needs to be set truncated. I definitely agree that "proper category theory" has to be done on a set level but there are many notions which are more general.

In my mind, if we remove the truncation assumption, we have "1-coherent oo-category theory". An example of where this might be useful in in proving the loop-susp adjunction. We can literally define a (1-coherent) functor loops and a functor susp. Show that they are (1-coherently?) adjoint and recover the equivalence that way. This is a silly example , but I have other adjunctions in mind as well.

I would image this change would actually let us use some of the category theory. I have currently sort of mirrored a lot of category theory for pointed types in my formalisation of smash coherence. I also had to write down a definition of monoidal product which might be useful in the category theory library too.

Of course, I don't think it is as easy as removing the truncation. And I don't imagine sticking the word "wild" everywhere is going to make the library nicer. Something to discuss.

[spitters]

Someone once developed such a library for wild categories in agda. Unfortunately, I cannot remember where I saw the presentation. https://ncatlab.org/homotopytypetheory/show/wild+category

[JasonGross]

I seem to recall trying this once. I think Yoneda breaks, possibly also the Hom functor (or at the very least you need to change what category it lands in). You also want it to build Cat, or else a lot of the theory would get significantly hairier, because equality of functors now needs to talk about equality of paths.

Furthermore, without the truncation assumption, it's no longer clear you can pull the tricks I do to get C^op^op to unify with C, because now the redundant path information wouldn't collapse. The library relies heavily on this sort of unification being judgmental, if I recall correctly, in building up the theory of (co)limits, adjoints, and comma categories.

[mikeshulman]

The suggestion is only to remove the assumption of truncation of hom-types from the definition of category (and perhaps put it into a typeclass that can be assumed explicitly when needed), not to add anything else to the definition (i.e. no coherence -- hence the adjective "wild"). Would that really break unification of double-opposites?

[JasonGross]

The definition of PreCategory already contains extra data beyond just wild categories + truncation assumption: https://github.com/HoTT/HoTT/blob/822172df522ea751841c6df10514e1b952285dc3/theories/Categories/Category/Core.v#L45-L75 In particular, we have both associativity and associativity_sym, and we have left_identity, right_identity, and identity_identity. Together with the truncation assumption, this duplication of data is harmless. And we need the data to preserve unification of double-opposites and related things. But what about when we don't have that assumption? It seems that to make our notion truly equivalent to a "wild category", we'd need to add coherence laws so that we were only carrying one copy of the assoc and so that identity_identity was coherent with one of the left/right laws. I don't object to moving the truncation assumption to a typeclass (well, except for the fact that it might mess up Cat), but it seems like we perhaps need a name other than WildCategory for the resulting structure?

[mikeshulman]

Right, I forgot about that. My initial suggestion (subject to revision, if it doesn't work) would be to just (re)move truncation and leave the duplicated data, so that what we have isn't quite the same as what other people have called a "wild category". My expectation is that such a "symmetrically wild category" would be just as good as an ordinary wild category for most any purpose we care about, and perhaps better because of double-opposite unification. It's easy to "symmetrize" an ordinary wild category, right?

Couldn't we just add the truncation assumption when defining the objects of Cat? Is it more complicated than that?

[JasonGross]

My initial suggestion [...]

Yeah, that seems fine to me.

It's easy to "symmetrize" an ordinary wild category, right?

Yes, in fact we have a "constructor" Build_PreCategory which does just that.

Couldn't we just add the truncation assumption when defining the objects of Cat? Is it more complicated than that?

Using ... a sigma type? A new record? Then morphisms of Cat will not just be functors, but have to turn these truncated categories back into symmetrically wild categories to use the existing type of Functor. There are probably places where I interchange "functor" and "morphism in Cat" (I think I define a pseudofunctor over category sliced over or under Cat or something, when doing (co)limits?), and we'd have to be a bit careful here. I'm not saying it won't work, just that I expect there to be complications getting everything to pass Coq's typechecker and type inference.

[mikeshulman]

Ok, sounds like the consensus is that if @Alizter (or anyone else) wants to experiment with this, it could be worthwhile.

Actually I just remembered there was some discussion of something like this back at #832 .

[JasonGross]

And here is some work I did on this a couple of years ago: https://github.com/JasonGross/HoTT/tree/yoneda-without-truncatedness-trunk

[JasonGross]

And maybe see also https://github.com/UniMath/UniMath/issues/54

[JasonGross]

And this is the thread that caused me to make the branch in the first place: https://groups.google.com/d/msg/homotopytypetheory/cYPhbT4HGcs/27-OWTEEavwJ

[Alizter]

Some more examples:

• (Wild) category of types with relations and relation preserving maps.
• (Wild) category of "graph diagrams" and "graph diagram maps".

Notably there are "functoriality results" related to these two which would best be encoded as a 1-coherent functor as discussed above.

Edit: I should have mentioned that these examples can currently be found in the library.

[Alizter]

tslil and I separately tried to remove the truncatedness assumptions in the Categories library however the workload is too great. Our current wildcat library seems to be better suited to our needs as we can add what we need when we need it. It would be nice to wildify the categories library eventually, but it seems like a lot of work for not a lot of gain.