swap the argument order in equational reasoning

[maxsnew]

Addressing https://github.com/agda/cubical/issues/998 .

Currently not building because the current solvers have some hacks in them related to equational reasoning that I haven't fixed because they might not be necessary after this change. It would be nice to have an example of how this helps with a solver. I have a category solver in a different repo that I'm currently using to verify that this helps.

In the stdlib they also changed other *-reasoning syntax. I'm not familiar enough with the stdlib to know where all of those would be. Additionally I haven't change ≡⟨⟩⟨⟩-syntax or _≡⟨_⟩≡⟨_⟩_ yet but they should be similarly adapted as well.

[felixwellen]

I think the problematic code can be removed safely, since it wasn't in use anyway. I'm just type checking that and will make a PR on your PR once it is through.

[felixwellen]

Here it is, just in case it doesn't show up automatically (not checked yet, but I guess it is good to merge into this PR):

https://github.com/maxsnew/cubical/pull/1

[felixwellen]

Type checks on my machine and I actually could just substitute the worst ringsolver-macro with another one, because the RHS is available now in equational reasoning.

[felixwellen]

As far as I can tell, that should be ready for merging - or do you want to change anything?

[maxsnew]

Looks good to me. Main thing I would want to add is a test that demonstrate it works with equational reasoning

[felixwellen]

Have you looked at the CommRingSolver/Examples? That shows it works in simple cases und you can check it won't work in more complicated cases. But this is due to a shortcoming of how deBruijn-indices are handled in the CommRingSolver. I think it would be good to rewrite the latter using more existing code for the reflection interface, which is not neccessarily in the cubical-library. So I would say that is out of scope here...

[maxsnew]

Oh I guess I missed those. LGTM then

[felixwellen]

Okay -> merging.