[ refactor ] add rawSetoid manifest fields to Algebra.Bundles.Raw

[jamesmckinna]

This tackles the second part of #2274 as a followup to #2491 by replacing the in-place definition of negated equality in Algebra.Bundles.Raw.* with a delegation to its definition in the underlying RawSetoid bundle via an additional rawSetoid manifest field.

Outstanding issues:

• should the new field itself be publicly exported throughout, rather than simply the negated equality, as previously?
• does this addition give rise to similar problems as those recently fixed by Mess around with IsSemiringWithoutOne reexports #2499 ?

[JacquesCarette]

"new field" ? I make a difference between a 'field' in a record and a definitional extension - they differ quite a bit. For example, you can only assign to fields (as seen when doing copatterns) and not extensions.

You can test what's in a module by putting the name of a module in a hole and then doing C-c C-o. This will list all the names that are visible in that module. That should let you figure out item 2.

[jamesmckinna]

Apologies. What you call a "definitional extension" I habitually call a "manifest field", and hence, sloppily, simply a field.

Mind you, it would be great if they were overridable in the same way as fields, as that would make emulation of haskell-style defaulting sooo much easier...

[JacquesCarette]

I'm fine with "manifest field" (though I'll keep using "definitional extension"). I guess it's shortening that to "field" that bugs me!

Yes, I too would like some kind of 'default' mechanism. Though I think that, in Agda, one ought to be forced to prove that the alternate definition is equivalent to the default one. Which I guess means that providing a default on something with no notion of equivalence would be disallowed. It certainly would be interesting to play around with that!