Algebra property reexports

[Taneb]

• Note that a RingWithoutOne is a SemiringWithoutOne
• Introduce new module Algebra.Properties.SemiringWithoutOne
• Re-export many algebraic properties (appropriately renamed) into the property files for larger algebraic structures, including all the new semigroup properties for semirings, both for addition and multiplication

[Taneb]

Ah - this is failing, in part because I assumed that what I was calling +-cancelʳ (specialization of Properties.Semigroup.cancelʳ to addition) matches the preexisting +-cancelʳ (addition is right cancellative). There needs to be some rethinking of names here.

[jamesmckinna]

Ah - this is failing, in part because I assumed that what I was calling +-cancelʳ (specialization of Properties.Semigroup.cancelʳ to addition) matches the preexisting +-cancelʳ (addition is right cancellative). There needs to be some rethinking of names here.

See also #2654 ... I think there this is (yet another) instance of systematic clash of different authors' mental models of what the qualifiers denote... ?

Er, no. It's because we accepted the Algebra.Properties.Monoid.cancel* in #2692 without thinking through the consequences wrt Cancellative operations. Sigh.

[jamesmckinna]

I've made (frankly unsatisfactory) suggestions as to how to rename things, otherwise I'd simply approve. This all looks like useful refactoring/filling in the hierarchy, but we do need to do something about these cancel lemmas...

[jamesmckinna]

Suggest, in view of the clash between naming of cancel properties, that you perhaps make these

Suggested change

	; cancelʳ to +-cancelʳ
	; cancelˡ to +-cancelˡ
	; cancelʳ to cancelʳ-+
	; cancelˡ to cancelˡ-+

ahead of trying to figure out a solution to his mess.

Shoutout to @JacquesCarette for input on this (the names come from agda-categories via Jacques and his students, I think).

[jamesmckinna]

Suggested change

	; cancelᶜ to +-cancelᶜ
	; cancelᶜ to cancelᶜ-+

for consistency!?

[jamesmckinna]

See below for the additive versions.

[jamesmckinna]

Ditto

[jamesmckinna]

move to a renaming block?

[jamesmckinna]

ditto.?

[jamesmckinna]

Actually, I think it might be easier to simply not export the 'offending' names, on the basis that

• this should guarantee that testing succeeds (?)
• that this doesn't commit to 'nonsense' names ahead of any refactoring/renaming in Algebra.Properties.Monoid

Thoughts?

[JacquesCarette]

In theory, this is good. In practice, clearly there are all sorts of problems. Which require non-trivial thinking, which I can't do right now. But will come back to this when I can.