The free Magma on a Set, resp. Setoid

[jamesmckinna]

This is a specimen instance of a general hierarchy, intended to be placed under Algebra.Bundles.Free.X, and to be reexported publicly by Algebra.Bundles.Free, cf. my comments on #1281, esp for comparison with @JacquesCarette 's work on agda-categories.

UPDATED: now with the 'free' homomorphism ⟦_⟧_ guaranteed by initiality, plus a whole bunch of stuff.

But: Magma seems easy, compared to all the others... ;-)

For discussion: is this the right way to proceed?
(I'm conscious that the (inner) module structure alone needs some tidying up)

[JacquesCarette]

Hmm, a lot of this can be made generic. [All of it can be generated, but that's a different story for another day.] I do have some code in the Theories and Data Structures repository that should be resurrected and cleaned up for that purpose.

Even if we agree to write a lot of this "by hand", there is tons to discuss regarding the details of the design. Certainly Magma is a good place to start; I'd suggest Pointed as the 'next' one to do, to see what patterns emerge.

I'll add doing a thorough commentary on this to my "to do" list.

[jamesmckinna]

Thanks for the prompt to think about automation, and I look forward to your detailed comments!

As to patterns present in the design, thinking a bit harder about being systematic with naming would be helpful... as would a bit more Setoid yoga to state when a function is actually a Setoid morphism... and other such niceties. UPDATED: a bit of that now done.

UPDATED: @JacquesCarette I squinted at your 2019 paper on Theories and Structures, and that prompted me to add the functoriality of map (but without any explicit Functor instance/structure/bundle). But I'm torn about the best way to tackle the (Raw)Monad structure on the PreFree functor: Magma, like Pointed, doesn't have any non-trivial equations, so its PreFree functor and Free functors coincide, but once you have a non-trivial algebraic theory more care is required. So I'd be much more tempted to do Monoid next... right now I'm (a bit) more concerned about the organisation and naming of the material in the PR at hand (never mind the hierarchical structure it calls into existence). Snatching at low(er)-hanging fruit, perhaps, when your vision of a more general/generic approach might be more compelling. But currently the library doesn't even handle Free structures directly anyway, so doing some experiments now, towards agreeing an eventual generic design, seems desirable.

[jamesmckinna]

Re: Pointed ... it doesn't unfortunately exist under the Relation.Binary hierarchy alongside Setoid.

I guess one of us should open an issue for this? #1957

[JacquesCarette]

Pointed qua theory induces Maybe; I'm sure you know that, but I'm just making sure we're talking about the same thing.

So I was picturing Pointed as belonging to Algebra not Relation.Binary.

[jamesmckinna]

Re; Pointed yes as to Maybe (but I would perversely insist on writing Syntax again in this instance, for the sake of 'generality'/'genericity').

(DELETED: discussion moved to #1957)

[jamesmckinna]

This last commit revealed another 'missing' item from the library: cf issue #1960 there seems to be no Bundled version of MagmaHomomorphism etc., with Algebra.Morphism.Bundles as the (obvious?) candidate place for such a thing to live?

Suggest also that I should refactor the Properties submodule to be based on a SetoidHomomorphism... at present there's too much unbundling! UPDATED: now done, both as temporary pathc here, and as a separate PR #1960

[jamesmckinna]

OK... after functoriality of the FreeMagmaFunctor, I think it's time to stop. FIXED.

One outstanding question: besides resolving the above review conversations, where should such a contribution live, assuming that we want it anywhere?

I chose Algebra.Bundles.Free.Magma, but perhaps Algebra.Free.Magma would be better?

[jamesmckinna]

Blast, I've screwed up reverting the bogus merge commit again... sigh.

I'll make a fresh PR. Double sigh.