Algebra.Bundles.SemiringWithoutOne fails to export setoid?

[jamesmckinna]

More specifically, Algebra.Bundles.Semiring does indeed export all of its corresponding substructures (down to setoid derivable via Algebra.Structures), while Algebra.Bundles.SemiringWithoutOne appears not to. Not quite sure how to fix this, but will update if/when I do... with a minimum (non-)working example.

EDITED: See the two Test files at Algebra.Properties.Semiring{WithoutOne} on this branch now minimised.

UPDATE: the problem seems similar to that described/solved in issue #1159 / PR #1174, and I think I have a solution, but I'm conscious of being out of my depth as to the arcane define/public re-export structure of the Algebra.* hierarchy, so reluctant to issue a PR about this... Which raises a separate question: how 'high' (=fewest operations, axiomatic properties) in the Structures (and hence Properties.BundleX.OperationY) hierarchy do we want certain things to live: eg distributivity of _*_ over sum, defined in #1462, placed it as a property of Semirings; @uzytkownik 's original contribution (from a year earlier) under #1287 placed it under SemiringWithoutOne... and AFAICT, it doesn't even need that much structure, only that of the theory pullback (which has no name) of SemiringWithoutOne and SemiringWithoutAnnihilatingZero. In pursuit of #1287, I'd be happy for everything to live under properties of Semiring, and leave the appropriate weakening of structure to subsequent refactoring... but I know that there are strong views about the ambient guiding principle of 'be no less general than you absolutely can', and I thought that this was worth flagging.

[jamesmckinna]

Will see if I can knock this off along the lines of @Taneb 's #1967 ... later.

[jamesmckinna]

Aaargh, this issue is really two:

• exporting setoid now DONE
• adding more diamonds to find a home for eg distributivity of _*_ over sum: WON'T DO

The first might be easy (but I feel faint thinking about it), but the second?

[jamesmckinna]

[deleted]
Stale *.elc: resolved by agda-mode compile

[jamesmckinna]

I now find myself in the uncomfortable position of having a solution, but one which I do not understand, and hence don't know if it will cause problems later if merged... :-(

UPDATED: the issue/diagnosis on the PR is that CommutativeMonoid failed to export setoid; instead, it simply exported the latter's isEquivalence field... which required some other Bundles to then have to explicitly re-export the negated equality relation symbol. Exporting setoid allowed/obliged such non-uniformity to be ironed out. Similar uniformities then emerge as part of ongoing investigations into #2096 and #2098...

[MatthewDaggitt]

But I definitely don't understand the agda2-mode behaviour as regards names brought into scope by public export... is this a bug?

Looks like a bug to me. Report on the Agda repo?

[jamesmckinna]

Hmm, resolved after an agda-mode compile.