METATHEOREM: remove the use of choice in Completeness

[codyroux]

Is your feature request related to a problem? Please describe.
Sadly, we use choice in the proof of completeness, to pick a substitution which "lifts" an interpretation into the free magma quotiented by the laws.

equational_theories/equational_theories/Completeness.lean

Line 106 in e56c7bc

theorem PhiAsSubst_aux {α β γ} (Γ : Ctx α) (φ : β → FreeMagmaWithLaws γ Γ) :

Describe the solution you'd like
Ideally, we'd determine whether that use of choice is required (I strongly suspect that it is not) and remove it if possible. It's likely some use of the excluded middle are unavoidable though.

Describe alternatives you've considered
The alternative here is to do nothing.

Additional context
Here is a gorgeous proof of the same (slightly more general, actually) theorem in Agda by Andreas Abel. One could simply carry out an identical proof. https://www.cse.chalmers.se/~abela/agda/MultiSortedAlgebra.pdf

[teorth]

While not essential to the rest of the project (at least, not yet), this is an aesthetically nice improvement to the proof, so if you want to volunteer for this project, be my guest. (It seems that you could also help get the ball rolling on formalizing the abstract nonsense chapter as well, which is a bit more tied to the rest of the project, so you could consider directing effort to that direction instead in the near-term. Of course it is up to you.)

[codyroux]

I'm having a rough work week, but if it's still up for grabs after I'd be happy to.

I should note that the Abel exercise doesn't actually trivially solve the problem (I now realize): it works in setoids rather than quotient types, so the "get a representative" function is trivially constructive: it's the identity. In some sense it proves something weaker: the models in which equality is an arbitrary relation are complete.

I'll have to take a closer look at the proof.