search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
367 stars 68 forks source link

Update to standard library 1.5 #242

Closed turion closed 3 years ago

turion commented 3 years ago

The standard library has been released at version 1.5 https://github.com/agda/agda-stdlib/issues/1386 :tada:

It was noticed by @iblech in https://github.com/NixOS/nixpkgs/pull/110830 that agda-categories uses the module Relation.Binary.OrderMorphism which has been deprecated. This should probably be fixed?

JacquesCarette commented 3 years ago

Yes, indeed it should. I welcome even partial PRs on this. I'm not likely to get time to fix this for at least 10 days.

sstucki commented 3 years ago

I'm a bit curious about the change of the definition of OrderMorphism in the stdlib. The old definition wasn't as uniform as the new one (when compared to the generic definitions) but it had less redundancy (as is evident in @MatthewDaggitt's PR #243). If one is actually working with posets, the new definition is a bit of a pain, it seems.

Would it not have been possible to keep both versions in the stdlib? Or at least add some helper functions/smart constructors that compute the redundant fields?

sstucki commented 3 years ago

Just to be clear, if an order morphism goes between two posets (as opposed to preorders) then the cong field is redundant because it follows from mono and antisymmetry. Hence one could define a helper (akin to those we have in other parts of the library) that fills in cong automatically.

turion commented 3 years ago

Hence one could define a helper (akin to those we have in other parts of the library) that fills in cong automatically.

Like what other helpers?

JacquesCarette commented 3 years ago

Like ntHelper and niHelper.

sstucki commented 3 years ago

... or categoryHelper. https://github.com/agda/agda-categories/blob/2080b4d6f87dff6fe807f8e8913e566c24cc0797/src/Categories/Category/Helper.agda#L32

There's lots of them in agda-categories. Of course, for OrderMorphism it would be better to put a helper in the stdlib. I'd be happy to write one and create a PR but I have no idea where best to put such helpers in the stdlib.

turion commented 3 years ago

Of course, for OrderMorphism it would be better to put a helper in the stdlib. I'd be happy to write one and create a PR but I have no idea where best to put such helpers in the stdlib.

Maybe it makes sense to have it as well in agda-categories at the beginning, because the stdlib will probably not make a new release just for that?

MatthewDaggitt commented 3 years ago

Would it not have been possible to keep both versions in the stdlib? Or at least add some helper functions/smart constructors that compute the redundant fields?

Yes, to both. So the old definition wasn't usable in many important cases because you didn't actually know that one of the relations was a poset and the point of establishing the morphism was to transfer the properties across in (see Data.Rational.Properties for an example). The new definitions are more general so can be used in both cases. You're right though I had missed the fact that some of the fields are redundant and that it's sometimes easier to work with the bundled form than the structure form.

I'll add the bundles and smart constructors to Relation.Binary.Morphism.Bundles in the standard library but probably won't make a new release unless some other bug comes up. I'll therefore make a cut-down version of the smart constructors for #243.

MatthewDaggitt commented 3 years ago

Opened https://github.com/agda/agda-stdlib/issues/1407 to address this.

sstucki commented 3 years ago

Splendid, thanks @MatthewDaggitt!

turion commented 3 years ago

Will you prepare a new release for agda-categories?

JacquesCarette commented 3 years ago

Yes. But first I was to bring in PR #240 as it seems ready.

iblech commented 3 years ago

Awesome that this could be fixed so quickly! :-)

How can I help with PR #240? Cutting a new release of agda-categories, compatible with standard-library 1.5, is the last thing to be done before we can release the new standard-library in Nix. :-) (We strive to offer an all-compatible package set, hence updating just standard-library but not agda-categories is not an option.)

JacquesCarette commented 3 years ago

The PR has been merged in now.

iblech commented 3 years ago

Super awesome, thank you very much Jacques! I'll immediately prepare the update for Nix.