API for duals

Stream: Equational

[Leo Shine]

Do we need an API to make it easy to prove facts about dual equations, I just did a PR here where I just adapted the proofs https://github.com/teorth/equational_theories/pull/86 but maybe for implications or non-implications that are a bit more involved it would be good to have something so we can avoid repeating ourselves

[Terence Tao]

Yes, once we have implemented equational#36 this should become possible, but currently we can only dualize one implication at a time.

[Cody Roux]

We should be doable now as a meta-theorem, by induction over proofs and using completeness, though the final step may have to wait for https://github.com/teorth/equational_theories/pull/135 to be finalized.

[Maja Kądziołka]

I don't think it would be necessary to use completeness here, just prove that the syntactic duality operator composes well with a similar one for concrete magmas, and then prove the implications by transporting everything through the "isomorphism"

[Terence Tao]

Just recording some relevant PRs and issues: equational#122 has some preliminary work on duality, and equational#174 asks to scan the list of outstanding open implications to see if any can be resolved by duality (this should eventually be part of the CI, done automatically every time new implications are added).

[Cody Roux]

Oops I have my own version as well, I have no attachement to it though. https://github.com/teorth/equational_theories/pull/165

[Cody Roux]

totally my bad, I didn't claim