Skip to content

Adds setoid export to Algebra.Bundles.SemiringWithoutOne (possible solution to #1917) #2093

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 2, 2023

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Sep 14, 2023

What I don't understand is why/how this solution is to be preferred over others (such as?), or whether this may break anything subsequently... nor how this problem came about in the first place... nor what, if any, CHANGELOG entry might be suitable to account for the fix.

@Taneb
Copy link
Member

Taneb commented Sep 14, 2023

As an aside I've been wondering if there's a good way to either test that this sort of thing is done right, or rewrite the library so all the re-exports are there by construction.

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Sep 14, 2023

Well, hence my mention of #1917 on #1967... and my hope that you will publish your big diagram at some point, as the source for exploring your "good way to test"/"rewrite the library"... but I'm glad it's not just me who feels this kind of things is too difficult to reliably debug 'by hand'!

UPDATED: What remains odd for me is that the explicit reexport of _≉_ is still present in a number of the Algebra.Bundles, yet does not give rise to the same ambiguity of names. So, for me at least, even the 'solution' offered here leaves questions as to whether there is a better, more systematic one, out there.

@jamesmckinna
Copy link
Contributor Author

status:ready modulo CHANGELOG of course...

@jamesmckinna jamesmckinna added this to the v2.0 milestone Sep 29, 2023
@jamesmckinna jamesmckinna changed the title Candidate solution to #1917 Adds setoid export to Algebra.Bundles.SemiringWithoutOne (possible solution to #1917) Sep 29, 2023
@MatthewDaggitt MatthewDaggitt merged commit f945a3b into agda:master Oct 2, 2023
@jamesmckinna jamesmckinna deleted the issue1917 branch October 21, 2023 14:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Algebra.Bundles.SemiringWithoutOne fails to export setoid?
3 participants