Comments (18)
There's an outstanding PR to make it compile with 2.5.4.2 that I need to take care of. It's essentially ready, so I should just make the tiny change myself that it needs. Then we can see. I have not tried it at all yet, so I just don't know!
from categories.
So I tried. I think it might have worked for 2.5.4.2, but it doesn't work for 2.6.
I think it's time for a redesign. For example, using Prop
rather than irrelevance. And more of the standard library for the various pieces of 'reasoning' that are inside this library.
from categories.
@JacquesCarette are you working on it already? do you have a repo available?
from categories.
I have started some work, but have pushed nothing, as I was still struggling with all the dependencies for just rebuilding the Categories.Category
module.
I was originally thinking of using my fork https://github.com/JacquesCarette/categories for doing the experiments. But I'm not even sure that's a good idea, as I'm pretty sure this will end up being a rebuild almost from scratch.
Lastly, I definitely want to rebuild this based on 2.6 as much as possible, and in an incremental way, as there does seem to be willingness (agda/agda-stdlib#652) to migrate this into stdlib.
from categories.
Long story short: I welcome any and all suggestions you may have as to how to proceed!
from categories.
it seems the library does not only depend on irrelevance but also K (in some part). I would prefer a relevant library because irrelence is an uninvertible loss of information, which I tend to avoid. I will experiment these couple days.
from categories.
https://github.com/HuStmpHrrr/agda-categories
I tried to define natural transformations and two compositions relevantly without using K and other postulations. it seems to work out well. do you have any concern?
from categories.
Thanks - I will try to look as soon as possible. But that may well be Friday.
from categories.
@HuStmpHrrr It really does seem to work quite well! Seems very much worth continuing along that path. Would you welcome PRs?
I'd like to try to do both Adjunctions (as I need them now) and Monoidal categories (to resurrect old work) as a further test.
It's also nice that you were able to do things via using more of the standard library, instead of homebrewed setoid reasoning.
from categories.
@JacquesCarette definitely I welcome PRs. I think I will just authorize you to push directly.
In fact I don't intend to make this my personal repo. do you know how to make it a project under the agda group?
from categories.
Thanks. And let me ask.
from categories.
@JacquesCarette were you invited into the Agda group? I am not, so I am hoping that you could create the project and push what exists. do you get a chance to tale a look?
from categories.
I did. I just didn't get a chance to create the sub-project yet. I'll do it today.
from categories.
Where by 'today' I meant within 24 hours... done now, and I've sent you a contributor request.
And I just realized that you're probably less than 5 kms for me! I live in Waterloo too.
from categories.
thx I accepted.
how come? but you work in Hamilton, no? so you commute far.
from categories.
History. I used to work in Waterloo (at Maplesoft), my wife still does. Yes, I commute far. But I'm now quite used to it.
from categories.
that is very cool. I just pushed the commits to the new repo so I think it's set.
from categories.
Since the new library works and is an almost 100% port, this is now obsolete, closing.
from categories.
Related Issues (17)
- Library does not build with agda trunk HOT 3
- Does not build on 2.4.2 HOT 1
- Foo
- Doesn't build with 2.4.2.3-rc HOT 2
- Several issues with 2.5.1.1 HOT 1
- Parse error with agda 2.5.2 HOT 4
- Delay Monad using sized types for ISetoids HOT 2
- Horizontal composition does not compile anymore in later version of agda HOT 6
- Lift HOT 1
- in stdlib-0.16 implicit argument of Lift is now explicit HOT 4
- Data.Product.N-ary in stdlib 0.16 have [] conflicting with Data.Vec HOT 1
- Relation.Binary.On moved to Relation.Binary.Construct.On in stdlib 0.16 HOT 1
- Categories.Comma dos not type check with stdlib 0.16 HOT 1
- Category & Functor need to be marked with eta-equality to satisfy 2.5.4.2 HOT 4
- Unsolved metas in Categories.Power.NaturalTransformation with 2.5.4.2 HOT 1
- Categories.Support.SetoidPi does not compile with stdlib 0.16 due to Relation.Binary.Indexed HOT 1
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 categories.