The algebraic theory of semigroups

[lowasser]

With the general free construction, having algebraic theories of all the various structures becomes substantially more useful.

Builds atop #1894 .

[lowasser]

The main thing about this PR is that it attempts to use naming schemas more appropriate to the current patterns in agda-unimath than the preexisting algebraic-theory-of-groups page.

[EgbertRijke]

One thing that occurs to me, is that when an algebraic theory is the object of definition, then the naming scheme is expected to be

...-Algebraic-Theory

Based on the standard naming scheme, I would expect the algebraic theory of semigroups be called

semigroup-Algebraic-Theory

and other names derived from it, such as:

signature-semigroup-Algebraic-Theory

type-semigroup-Algebraic-Theory

and so on.

I'd be happy to discuss other possibilities too, and hear why you've chosen your scheme before making a final decision.

[lowasser]

My interpretation of the distinction between these naming schemas is that semigroup-Algebraic-Theory is meant to parse (disambiguating description)-(result type), and algebraic-theory-Semigroup is meant to parse (result type)-(Namespace/Object). I think both parsings are relatively common in unimath, though they are rarely so ambiguous. (And reviewing in retrospect -- I could've sworn that the term "namespace" was used to describe functions associated with things we are naming with capital letters, but that doesn't seem actually true; you seem to use it consistently to describe what I'd call "packages.")

I admit I'd tend to read semigroup-Algebraic-Theory as "the semigroup associated with some particular Algebraic-Theory," though I suppose that's equally nonsensical to the reading of algebraic-theory-Semigroup as "the Algebraic-Theory associated with some particular Semigroup."

Additionally, the structure of universal-algebra as currently written doesn't make a signature or an operation part of an Algebraic-Theory; there is certainly no signature-Algebraic-Theory. Instead, the signature is a parameter of Algebraic-Theory. This makes me substantially less happy to write signature-semigroup-Algebraic-Theory, so then...what should the signature be called? It could be semigroup-signature, and then semigroup-operation or operation-semigroup-signature?

I still think the names I have in this PR are more sensical, but I'm more willing to be persuaded after thinking through this comment that at least the thing of type Algebraic-Theory could be semigroup-Algebraic-Theory.