Incompatabilities

[HuStmpHrrr]

I am wondering how far is it to resolve the incompatibilities of this library to up-to-date agda?

Agda has reached 2.6 and I am eager to try in near future but I am not sure how far is it for this library to be ready.

[JacquesCarette]

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!

[JacquesCarette]

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.

[HuStmpHrrr]

@JacquesCarette are you working on it already? do you have a repo available?

[JacquesCarette]

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.

[JacquesCarette]

Long story short: I welcome any and all suggestions you may have as to how to proceed!

[HuStmpHrrr]

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.

[HuStmpHrrr]

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?

[JacquesCarette]

Thanks - I will try to look as soon as possible. But that may well be Friday.

[JacquesCarette]

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

[HuStmpHrrr]

@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?

[JacquesCarette]

Thanks. And let me ask.

[HuStmpHrrr]

@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?

[JacquesCarette]

I did. I just didn't get a chance to create the sub-project yet. I'll do it today.

[JacquesCarette]

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.

[HuStmpHrrr]

thx I accepted.

how come? but you work in Hamilton, no? so you commute far.

[JacquesCarette]

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.

[HuStmpHrrr]

that is very cool. I just pushed the commits to the new repo so I think it's set.

[JacquesCarette]

Since the new library works and is an almost 100% port, this is now obsolete, closing.