Quasigroup as in Universal Algebra section on Wikipedia or using Latin square property? about agda-algebra HOT 5 CLOSED

That diagram is correct, but it is not 'structural', in the sense that if you go through Loop, Group will have 3 binary operations (and no unary operations). The unary operation will be definable, and with associativity, the two binary operations inter-definable as well.

So there will be a type equivalence between Group (defined as in the stdlib) and AssociativeLoop.

from agda-algebra.

Note that if we could use \ and / for the divisions, that would be nicer, I think.

To me, the better definition of quasigroup is the one based on universal algebra, with 2 division operators. This is because the result is an algebraic variety.

We cannot define a group to structurally extend a loop, because it would contain many redundant operations. It is then a theorem that an associative loop is a group and vice-versa. It is not a structural result.

Does that make sense?

from agda-algebra.

Note that if we could use \ and / for the divisions, that would be nicer, I think.

Yes I agree. I will change it.

Define group I meant using "algebra hierarchy" as in this diagram. In stdlib it is defined using Monoid (With 1 binary operation, 1 unary operation & 1 element). But what if we want to define using Loop ( and Loop using Quasigroup) ? We should potentially get same instance of group.

from agda-algebra.

Got it. Thanks!

from agda-algebra.

Name for quasigroup identites and division operator is updated as suggested.

from agda-algebra.