REFACTOR I: Reversing the ordering on laws

Stream: Equational

[Terence Tao]

This is an announcement of the first of possibly three refactorings of the entire Lean codebase: following the outcome the polls at #Equational > Metatheory: meta-thread , I have opened equational#199 to reverse the ordering on equational laws to align with Mathlib.

This one is the smallest and least disruptive refactoring, because this ordering is not used widely in our Lean codebase, so I believe this should be relatively simple to implement, and can be done in advance of any other refactorings (namely, the potential refactorings to change the ordering on variables, and to switch from [Magma] to [Mul]). I have already updated the blueprint to reflect this new convention.

As a related policy change, we will now have the following recommendations for Hasse diagrams going forward:

Hasse diagrams will be oriented with the largest element x=x (in the new ordering) ontop and the smallest element x=y on bottom, and arrows should be depicted by upwards implication arrows => (or left unoriented, if implication arrows are not available).

Legacy Hasse diagrams created before this policy change do not need to be updated, but a note should be attached to any documentation referencing these diagrams to indicate the reversed orientation.

I will now go ahead and add this guidance to CONTRIBUTING.md and to the places in the documentation that reference visualizations. I don't know if there are any of the graph visualization tools in the codebase need to be adjusted in view of this policy, but perhaps this can be done by the creators of each individual tool separately, without the need for an overarching refactor?