Add some very simple properties about algebraic structures.

[sstucki]

Concretely: add proofs that the basic structure of magmas, semigroups and monoids are preserved if we switch the arguments of their binary operation.

[gallais]

Should this go in Relation.Binary.Construct.Flip?

[sstucki]

Should this go in Relation.Binary.Construct.Flip?

I don't think so because we're flipping the binary operation, not the associated equivalence relation. If anything, it should go into a new module Algebra.Construct.Flip, but I figured Algebra.Consequences.Base would do for now. 🤷

[MatthewDaggitt]

Okay so this should all definitely go in an Algebra.Construct module. The question is what under what name.

I think it should be Algebra.Construct.Converse not Algebra.Construct.Flip to match the semantics of Relation.Binary.Construct.Converse/Flip. The former does not flip the underlying equality relation, whereas the latter does. This PR does not flip the equality and therefore Converse it is.

[MatthewDaggitt]

See #1751 for how such a module should look like.

[sstucki]

I think it should be Algebra.Construct.Converse not Algebra.Construct.Flip to match the semantics of Relation.Binary.Construct.Converse/Flip. The former does not flip the underlying equality relation, whereas the latter does. This PR does not flip the equality and therefore Converse it is.

But Converse doesn't make sense if flip is applied to a binary operation. When you exchange the arguments of an relation, you get it's converse, but when you exchange the arguments of a binary operation you don't get it's converse, you just get another operation. Flip makes a lot more sense IMO.

[MatthewDaggitt]

Okay so what are we going to call the module that flips both the binary operation and the underlying equality?

[Taneb]

Do we ever want to flip the underlying equality? We know it's symmetric

[sstucki]

Okay so what are we going to call the module that flips both the binary operation and the underlying equality?

Honestly, flipping an equality relation doesn't make a whole lot of sense to me as it's already symmetric. But I guess there was a good reason (that I don't know about) to do this in the Relation.Binary hierarchy. If it's ever necessary to flip the equality in the Algebra hierarchy, we could have submodules Flip.{Op,Eq,OpEq} at least that would make it clear what's going on.

[MatthewDaggitt]

Do we ever want to flip the underlying equality? We know it's symmetric

So Binary.Construct.Flip predated my involvement of the library, so it was needed "first" but I'm unsure what for. I added Converse later, because Flip was deeply inconvenient. In general though, I've learnt that if something seems a sensible operation then someone will need it somewhere even if I can't come up with a use case immediately.

If it's ever necessary to flip the equality in the Algebra hierarchy, we could have submodules Flip.{Op,Eq,OpEq} at least that would make it clear what's going on.

This seems like an excellent suggestion to me. So this module would be called Algebra.Construct.Flip.Op? We should be consistent though and refactor the Relation.Binary.Construct modules to follow the same pattern. Let's not do it in this PR though.

[sstucki]

This seems like an excellent suggestion to me. So this module would be called Algebra.Construct.Flip.Op? We should be consistent though and refactor the Relation.Binary.Construct modules to follow the same pattern. Let's not do it in this PR though.

OK, I'll create that module and move the proofs there then. But to be clear: that module will contain the "generic" proofs, the derived proofs involving bundles of algebraic structures should still go into separate modules under Algebra.Properties, right?

[MatthewDaggitt]

I'm not quite sure what you mean by "generic" proofs. All the proofs that you've added should live in the new module. If you want to (no requirement to though) you could also keep the statements in the places you've got currently, but use the new module to prove them. Does that make sense?

See for example how Relation.Binary.Construct.NonStrictToStrict contains all the proofs to strictify a relation, and Relation.Binary.Properties.Poset then makes use of it.

[sstucki]

Oh, I see now in Relation.Binary.Construct.Flip that there is a "Structure" and "Bundles" section that implements the per-structure and per-bundle properties. Then the separate modules in Properties are no longer needed. 👍

[sstucki]

OK, version 2 ready for review. Now everything is in a single module called Algebra.Construct.Flip.Op as discussed previously. I threw in proofs for some additional structures for good measure (everything with a single binary operation).

[MatthewDaggitt]

Other than that, looks great!