Ring fails to re-export various raw structures

[Taneb]

I haven't investigated to see how big this problem is, but Algebra.Bundles.Ring is missing at least +-rawGroup and rawNearSemiring

[jamesmckinna]

So... Algebra.Bundles.Raw.Ring since #1755/#1810?

[Taneb]

@jamesmckinna I don't think that's what I meant. I meant that the Ring bundle, with the laws, does not expose anything called +-rawGroup : RawGroup c l directly. You have to go through either +-group or rawRing to get it. It's been a long while so I can't remember why this came up, but note that some things (for example homomorphisms) are defined over the raw bundles so it's reasonable to want to get at any of the raw sub-bundles easily, and these two felt like obvious omissions.

[jamesmckinna]

OK. I think I had myself only meant that even these definitions had moved. But yes, if Ring doesn't export them, then they should be added. But PR #1867 is still in review, and I'm loathe to add more to it now, especially if it is blocking on my having failed to clean up the commits properly.

That said, the public exports in Algebra.Bundles.Raw from rawRing do export the raw bundles you want, so... doesn't a open import Algebra.Bundles.Raw do the trick? Apologies if I am being obtuse (I find the Algebra hierarchy, and the (very!) complex re-exporting discipline very hard to get my head round).

UPDATED: in the light of thinking a bit harder, and avoiding overlapping exports, does adding

  open RawRing rawRing public
    using (rawRingWithoutOne; +-rawGroup)

to the definition of Ring solve the problem? Or should there be a more fine-grained analysis of what gets exported by opening the Semiring (to export rawNearSemiring) and RingWithoutOne instances?

[jamesmckinna]

I think I had intended to remove the 'fixes' linkage to #2254 to keep this open?
Do you want to (re-)open this @Taneb , or open a fresh issue on eg. "Algebra.Bundles.* should re-export all Raw sub-structures"?