Quasigroup as in Universal Algebra section on Wikipedia or using Latin square property?

[Akshobhya1234]

In stdlib, we define Quasigroup as magma with inverse as in . But in Ncatlab they mention that "In the absence of associativity, it is not enough to say that every element has an inverse element; instead, you must say that division is always possible."

https://github.com/Akshobhya1234/agda-NonAssociativeAlgebra/blob/5757fb6638283a816814b1049530b650d330fa4c/src/Quasigroup/Structures.agda#L30

Here we define quasigroup identities as in the Universal Algebra section on Wikipedia with 2 division operators.

https://github.com/Akshobhya1234/agda-NonAssociativeAlgebra/blob/5757fb6638283a816814b1049530b650d330fa4c/src/Quasigroup/Definitions.agda#L13

Also latin square property is defined
https://github.com/Akshobhya1234/agda-NonAssociativeAlgebra/blob/5757fb6638283a816814b1049530b650d330fa4c/src/Quasigroup/Definitions.agda#L25

If we define as in the Universal Algebra section on Wikipedia, It will have 3 binary operators. How can we extend this to define Loops and Group?

[JacquesCarette]

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?

[Akshobhya1234]

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.

[JacquesCarette]

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.

[Akshobhya1234]

Got it. Thanks!

[Akshobhya1234]

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