[ refactor ] Algebra.Structures.KleeneAlgebra and Properties

[jamesmckinna]

This completes one possible approach to fixing #3003, building on #3030 (on which this blocks) by plumbing in the partial order structure (definable in a CommutativeBand, but here only locally to IsKleeneAlgebra), and correcting the types of the Algebra.Structures.IsKleeneAlgebra.star* fields to use this _≤_ relation.

TODO:

• fix Algebra.Properties.KleeneAlgebra (a lot more work required!), but this is a substantive issue, echoing @Taneb's question about what axiomatisation (and hence which admissible properties) we actually want to have? UPDATED: now have added Conway C11 and C12, which weren't even in the original module! Not sure if we want/need C14n?

[jamesmckinna]

Oh, there I go again blundering into Algebra.Structures thinking I'm so smart, and immediately banging my head against Relation.Binary.Construct.NaturalOrder.{Left|Right}, which ... are of course the opposite ordering to the Kleene one.

Suggested refactoring:

• Minimum: put everything back in IsKleeneAlgebra
• Then: move properties out of that structure into Algebra.Properties.KleeneAlgebra
• Ultimately? Maybe follow @MatthewDaggitt 's development of NaturalOrder, and install Relation.Binary.Construct.NaturalOrder.Kleene? Suggestions welcome!

[JacquesCarette]

It took me a frightfully long time to come around to the opinion that this change is the right one. So at the design level, this is an 'approve'. But there's a tiny nitpick before we can merge.