agda-stdlib
agda-stdlib copied to clipboard
agda
Add some type relations and isomorphisms
Upstreaming some functions that I've used to prove things about sets (not the Agda kind).
@WhatisRT any progress on the suggested changes? This should be easy to merge once you've done that...
I've added the changes to the CHANGELOG. I don't really understand what's the final verdict on the naming, should I change some of the names or not?
Yes, some of the names do need changing from what's in your PR. But some of the name changes you did do were not necessary!
I think that it would be good to try to merge this sooner rather than later, and AFAICT, it's down to agreeing names for the new additions... can we converge on mutually agreeable suchl!?
Looks like the master merge broke the build?
Nope... (I think) it's a CI thing... the rebuild of alex and happy which fails even before the attempted master merge is tested...
Reading the comments, it looks like we have got consensus on the names?
Reading the comments, it looks like we have got consensus on the names?
Yes, I'd been waiting on @WhatisRT to update this PR, but if you're keen to merge now (and for sure, this PR prompted me to think harder about some other type isos which might usefully be added downsream, esp. as regards refactoring Data.List.Relation.Binary.BagAndSetEquality (again!)), I'd be happy to push updates from my end...
Sorry, I think I missed some of the naming suggestions. But it seems you all have way stronger opinions about that than I do so I'd rather let you do the final adjustments.
I think if @JacquesCarette or @MatthewDaggitt can resolve the questions about level polymorphism and its impact on names (I managed to confuse myself too much over this to do so :-() then following @WhatisRT 's most recent comment, then you should make those changes yourselves and merge!
Looking again at all this: the less/insufficiently polymorphic versions of the distributive laws are also present in Data.Product.Algebra, so it's tempting to argue for making the (possibly) breaking change of making Function.Related.TypeIsomorphisms carry only the more polymorphic version, and re-implement the less polymorphic versions in Data.Product.Algebra using that functionality? (Or vice versa?)
Also (but separate from this PR): in each module, assoc for each of sum and (non-dependent) product are less/insufficiently polymorphic... suggesting that the library design might benefit from larger scale rethinking of these questions... or have I misunderstood something fundamental to what's going on here? UPDATED Issue #2489
Requested changes from @MatthewDaggitt have been done, as verified by @gallais @jamesmckinna and I. Merging.