Redundancy in definitions for pre-categories and categories about cubical HOT 15 CLOSED

Or we could just have wild categories independent of categories, as it seems to be in Coq-HoTT. If it is renamed as "Wild" and in a separate folder, people are probably deterred from using it accidentally, when they actually want to use categories.

from cubical.

We bundle h-set assumptions into the structure also in algebra. The UniMath library had the has-homset assumption separate and it was a big mistake in the end, see e.g. UniMath/UniMath#362. So I don't think we should pull it out

from cubical.

Great, then I'll just implement that.

from cubical.

What are precategories used for? They don't seem to be used for much in the categories library so I think we should remove support for them unless we have a compelling reason.

from cubical.

I am pretty sure they are used somewhere in homotopy theory. I think the right thing to do would actually be:

• rename them to wild categories, because that seems to be more adopted
• refactor code on category theory to use wild categories (I don't know how realistic that is)
• base more category theory on (univalent) wild categories

I think I don't know enough to really say how reasonable that is, but I think it could be great to apply category theory to, say, the univalent wild category of types and functions.

from cubical.

I just noticed #973 was mentioned which introduced the application I was thinking of - so besides that there is probably nothing.

from cubical.

I'm not totally against it, but it would certainly be a big change. In a sense it would match the style of the rest of the library, where we usually establish hLevels on the side rather than bundling them with structures. This would have the downstream effect of basically every categorical construction also needing to characterize its hLevels, but this is a general issue with HoTT afaict. Doing a grep for isSetHom I count 150 lines that mention it.

So I can see an argument on principle for it, but I don't ever foresee using it so it would probably just be annoying for me personally if this change were made.

from cubical.

Ok, I see. I just wanted to raise the principle point ;-)
Maybe other people have something to say about this, but I certainly don't insist on anything, since I am not using much of the category theory anyway.
So I would be also fine with moving things to non-wild/pre categories if that's just more practical for everyone.

from cubical.

I was thinking of something like this: #1103

from cubical.

We bundle h-set assumptions into the structure also in algebra.

I don't think we made the right choice, but it didn't really bite us yet.

The UniMath library [...]

I wonder how they are dealing with all their 2-/bicategories then (but I am too lazy now to take a look).

In any case, I don't propose to change the current definition. If at all, I would be for having something separate, following Coq-HoTT. I might work on that some time, just out of curiousity what can be done with wild categories.

from cubical.

Did you suggest to refactor @aljungstrom 's code to use Categories?
Otherwise, I can just complete the PR #1103 by removing precategories and making Axel's code use wild categories.

from cubical.

@felixwellen I'm not sure if that theorem makes sense phrased in terms of plain categories. I'm all for the second suggestion however!

from cubical.

We bundle h-set assumptions into the structure also in algebra.

I don't think we made the right choice, but it didn't really bite us yet.

Me neither -- it has bitten me, actually... For instance, I've recently had to redefine finite sums over elements in (definitely not set-truncated) H-spaces and reprove various lemmas about them. I really think we should try to move out the h-set assumptions and have things like wild groups, wild rings, etc. But that seems like a lot of work so... maybe in the future....

from cubical.

Yeah, maybe in the next life/library ;-)

More seriously, it might make sense to add parts of the wild hierarchy when we need it. For example, it seems to make a lot of sense to base solvers for algebraic structure on the wild versions (if possible, I don't know it in all cases). And in that case as the only downside I can see, there is one forgetful map and maybe some slight one-time trouble with the reflection code.

from cubical.

Solved with #1103

from cubical.