akshobhya1234 / agda-algebra Goto Github PK

Wait for stdlib release 2.0 to setup workflow.

When defining direct product of quasigroup as

quasigroup : Quasigroup a ℓ₁ → Quasigroup b ℓ₂ → Quasigroup (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
quasigroup M N = record
{ Carrier = M.Carrier × N.Carrier
; ≈ = Pointwise {! M.≈ !} {! !}
; ∙ = zip M.∙ N.∙
; \ = zip M.\ N.\
; // = zip M.// N.//
; isQuasigroup = record
{ isEquivalence = ×-isEquivalence M.isEquivalence N.isEquivalence
; ∙-cong = zip M.∙-cong N.∙-cong
; \-cong = zip M.\-cong N.\-cong
; //-cong = zip M.//-cong N.//-cong
; leftDivides = (λ x y → M.leftDividesˡ , N.leftDividesˡ <> x <> y) , (λ x y → M.leftDividesʳ , N.leftDividesʳ <> x <> y)
; rightDivides = (λ x y → M.rightDividesˡ , N.rightDividesˡ <> x <> y) , (λ x y → M.rightDividesʳ , N.rightDividesʳ <> x <> y)
}
} where module M = Quasigroup M; module N = Quasigroup N

It says "Cannot resolve overloaded projection ≈ because it is not applied to a visible argument when inferring the type of M.≈"

@JacquesCarette Can you have a look at it.

Find better names for MoufangIdentity ?

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?