Update to standard library 1.5

[turion]

The standard library has been released at version 1.5 agda/agda-stdlib#1386 🎉

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

[JacquesCarette]

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]

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]

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]

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]

Like ntHelper and niHelper.

[sstucki]

... or categoryHelper.

agda-categories/src/Categories/Category/Helper.agda

Line 32 in 2080b4d

categoryHelper : ∀ {o ℓ e} → CategoryHelper o ℓ e → Category o ℓ e

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]

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]

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]

Opened agda/agda-stdlib#1407 to address this.

[sstucki]

Splendid, thanks @MatthewDaggitt!

[turion]

Will you prepare a new release for agda-categories?

[JacquesCarette]

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

[iblech]

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]

The PR has been merged in now.

[iblech]

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