Comments (15)
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.
Related Issues (20)
- Duplication of code in the library HOT 3
- Note licence exceptions HOT 2
- Slightly more generalized universes HOT 2
- Remove `isSet` accessors for algebraic structures? HOT 3
- Change the Constructor Name of Sequential Colimits HOT 2
- CI workflow with current agda master HOT 5
- Additions to the powerset module HOT 2
- Some Files are never checked HOT 6
- Suggested heap size for CI HOT 1
- SumMap in Algebra.Ring.BigOps should come from Semirings /Monoids HOT 1
- `make` fails on macOS Sonoma 14.2.1 with Apple Silicon HOT 1
- Algebraic geometry HOT 2
- Figure out why the CommRingSolver doesn't work in this case HOT 5
- Make the CommRingSolver work better with concrete rings
- More elegant construction of ZariskiLattice HOT 2
- Solver for wild categories
- arithmetic operations of Cubical.Data.Rationals is super slow HOT 1
- Naming Convention for Disambiguation HOT 1
- `__IMPOSSIBLE__` error in SSet but not in Set HOT 1
- Formalizing Devalapurkar & Haine
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from cubical.