Quasigroups

[djspacewhale]

Introducing a new folder that, so far, defines quasigroups and loops (unital quasigroups).

[fredrik-bakke]

You haven't defined what the symbols r/ and l/ mean. Are these supposed to be / and \?

[djspacewhale]

I changed the notation from / \ to r/ l/ as the standard forward-slash is apparently reserved for lambda expressions. I see later down you suggest introducing a different Unicode representative so I think this can broadly pend that.

[fredrik-bakke]

The justification for creating a new namespace for quasigroups is unclear to me. Why do you not wish to put this in group-theory? Notice that we also have semigroups and monoids in group-theory. I must admit I'm not familiar with the theory of quasigroups, is the nature of the theory very different from group-theory? Given its name, I would guess not, and then it might be appropriate to have it in group-theory.

[djspacewhale]

Truthfully I'm approaching this formalization of quasigroups as a way to learn about them, so I'm not an expert on the broad theory. Including them in the group-theory namespace could make sense - groups are simply unital associative quasigroups, anyways - but the applications seem rather different; say, finite quasigroups classically correspond to latin squares, and their representation theory is much subtler.

I don't want to step on toes too aggressively being a new contributor but the current namespace convention is a tad frustrating for me. Finding definitions is easier using the website and its search bar, but searching monolithic namespaces by hand is not as elegant as, say, using a hierarchy of namespaces a la cubical. I did think about creating a subnamespace group-theory/quasigroups but as this convention does not exist currently I held off. Has this (re)organization been discussed before?

[EgbertRijke]

@djspacewhale, that is totally fine. I don't think you are stepping on anyone's toes, and your contribution is most welcome! Learning and formalizing at the same time is a great strategy to really get to the bottom of a subject, I use that strategy too. To that end, would you be willing to cite standard references for you definitions, such as

Pflugfelder. Quasigroups and Loops: Introduction?

We have a references.bib file in the root folder and there are guidelines about how to include a bibliography at the end of a file. The situation could be improved by now, but it used to be the case that the definition of quasigroups and semigroups was wrong on wikipedia, so it is important to follow a standard reference.

I also think developing quasigroups in the group theory folder could make sense, because some definitions and results about quasigroups will be more general and it would be a natural setting for comparing the two developments. On the other hand, I do understand why you initially chose to create a setup in a separate namespace: The nonassociative case is actually quite different and the group-theory name space is quite large, containing many different concepts.

We are aware of the organizational conventions of the cubical library, and other libraries as well, and we have deliberately chosen our current library organization. I personally find other library organizations a bit chaotic, and the one-concept-per-file principle is the cleanest in my view. It is also good to keep in mind that the choices for a library organization are tied to the purpose of the library: In cubical the goal is to facilitate formalization related to current research, which agda-unimath also hopes to facilitate, but agda-unimath has an important secondary purpose, which is to develop an informative resource where ultimately the library webpage could serve as a nlab-style website where you can find precise definitions and infomation about how concepts are interrelated. From that point of view, an organization with concept.base and concept.properties modules where concept.properties becomes a dumping place for all sorts of properties is not helping us at all, and what would be in concept.base in cubical could often be spread out over several pages in agda-unimath, each its own concept.

I hope this explanation helps!

[djspacewhale]

I actually don't have a reference text and have been formalizing roughly what's on Wikipedia and the nlab, cross-referenced with arxiv papers that arise in searches. I'll look for that text though. It's of course not the morally healthiest approach, and I'm no longer a student so sourcing texts may be a bit harder, but I'll find a better primary source!

I also appreciate agda-unimath's goal of being a readable informative source and this knowledge-for-the-people element is one reason I chose to contribute here rather than, say, cubical (long-term I'm also interested in modal type theory and applications to synthetic math, a project that appears at technical odds with cubical). My thought was less around, say, having one groups.base defining everything to do with groups, but more around using subfolders to consolidate "subareas" of knowledge, say, putting abelian stuff in group-theory/abelian-groups/ and so on. That said, I'll respect how the library is currently organized, and Fredrik's notes about separating e.g. left/right quasigroups into their own files is a good note for following the one-concept-per-file principle that I'll incorporate.

[fredrik-bakke]

Private definitions are against our conventions. But... since we're discussing changes to our syntax conventions currently, maybe I can use you as a test dummy? I have an idea for how we might go about having operators like these in the library

[fredrik-bakke]

If you add the below module, then you can "open" the syntax elsewhere using open structure-syntax-Quasigroup Q, to access these operators for your chosen quasigroup Q, instead of using private definitions as you do currently.

Suggested change

	```
	```
	### Quasigroup structure syntax
	```agda
	module
	structure-syntax-Quasigroup
	{l : Level} (Q : Quasigroup l)
	where
	_*_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q
	_*_ = mul-Quasigroup Q
	_l/_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q
	_l/_ = left-div-Quasigroup Q
	_r/_ : type-Quasigroup Q → type-Quasigroup Q → type-Quasigroup Q
	_r/_ = right-div-Quasigroup Q
	```

[fredrik-bakke]

We could also consider using the division slash ∕ and reverse solidus operator ⧵ unicode characters for right and left division respectively. These are supposed to be mirrored characters, and semantically they're the right symbols. There's no agda-input sequence for them though, so this requires adding them to our list of special characters. Might still be worth considering though.

[fredrik-bakke]

Here are some formatting and naming suggestions. Overall you implement many of our conventions well. Our conventions can be quite overwhelming to newcomers, so please don't take my comments as criticism. Your work is overall quite nice.