Bump stdlib to 2.0 - Githubissues

agda / agda-categories

A new Categories library for Agda

https://agda.github.io/agda-categories

MIT License

366 stars 68 forks source link

Bump stdlib to 2.0 #406

Closed Taneb closed 9 months ago

Taneb commented 9 months ago

Closes #405. Supercedes #352.

I ran into difficulty trying to make Categories.Yoneda work with the new function hierarchy so I'm opening this as a draft.

Many of the changes could be made tidier.

Difficulties encountered so far:

Categories.Category.Instance.Setoids and Categories.Adjoint.Mate could both do with a definition of equality of functions between setoids. I've inlined it for the former but didn't for the latter, because we just want the relation and it'd be too much of a mess to define it there locally too.
I got sufficiently confused by Categories.Yoneda that I bounced off it. I may give this another go at some point.

Other maintainers of the library are explicitly invited to contribute to this PR.

Taneb commented 9 months ago

Status: I've been working through the modules in alphabetical order. I've skipped Categories.Adjoint.Mate because it would hugely benefit from having a definition of equality of functions between setoids somewhere, and its dependents. Currently up to Categories.Category.Instance.FamilyOfSetoids, but I won't have much time to work on it in the next few days

JacquesCarette commented 9 months ago

Thanks. I'm hoping to be able to push it forward this weekend.

It will definitely make sense to create some helper functions that ought to end up in stdlib 2.1, but can live in agda-categories for a single version.

Taneb commented 9 months ago

Wow, @JacquesCarette, you've stormed through that!

JacquesCarette commented 9 months ago

I ended up spending close to 12 hours yesterday single-mindedly pushing through this. I'd definitely appreciate a review @Taneb . I know there's quite a few things to clean up, but that's so much easier than the first pass.

JacquesCarette commented 9 months ago

(I'm going to use the review facility to leave additional notes for myself)