Redundancy in definitions for pre-categories and categories

[mortberg]

https://github.com/agda/cubical/pull/973 introduced some redundancy for pre-categories and categories. This could probably be streamlined to avoid code duplication

[maxsnew]

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.

[felixwellen]

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.

[felixwellen]

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

[maxsnew]

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.

[felixwellen]

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.

[felixwellen]

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.

[felixwellen]

I was thinking of something like this: #1103

[mortberg]

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. https://github.com/UniMath/UniMath/issues/362. So I don't think we should pull it out

[felixwellen]

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.

[felixwellen]

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.

[aljungstrom]

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

[felixwellen]

Great, then I'll just implement that.

[aljungstrom]

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....

[felixwellen]

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.

[felixwellen]

Solved with #1103