Cannot resolve overloaded projection _≈_ about agda-algebra HOT 10 CLOSED

One way to find out is to put ≈ in a hole, and do C-c C-w (for 'where', I think), and it will tell you where the definition(s) come from. (I think the documentation says "hy in scope")

from agda-algebra.

Yes, that's probably a good idea.

from agda-algebra.

I think I found the issue. It depends on how the quasigroup is defined in stdlib. I will create an issue in stdlib to change the definition.

from agda-algebra.

Have you tried M._≈_ instead? That's the real name of the function.

from agda-algebra.

Have you tried M._≈_ instead? That's the real name of the function.

That is exactly the issue. We cannot use M._≈_.

from agda-algebra.

But that makes no sense - that names comes from a module, and it shouldn't be overloaded at all. Can you provide a bigger explanation?

from agda-algebra.

What I don't understand is how/where two version of ≈ as in-scope in M. I can understand that that's the problem.

from agda-algebra.

What I don't understand is how/where two version of ≈ as in-scope in M. I can understand that that's the problem.

Got your question. To be honest even I am confused. The agda error will not make it clear as to where two version of ≈ is in-scope in M. (Could it be from Magma that is defined in same file?) But I think we will face similar issue when we try to define direct product for Lattice.

from agda-algebra.

But for now this issue is resolved with the current changes proposed to quasigroup in stdlib.

from agda-algebra.

@JacquesCarette I got the issue. We had 2 instances of _≈_ one from Quasigroup and other from RawQuasigroup when we say

open RawQuasigroup rawQuasigroup public
using (_≈_; //-rawMagma; \\-rawMagma; ∙-rawMagma)

in Quasigroup

To overcome this with we could remove _≈_ like
open RawQuasigroup rawQuasigroup public
using (//-rawMagma; \\-rawMagma; ∙-rawMagma)

from agda-algebra.