agda
The free `Magma` on a `Set`, resp. `Setoid` [bis]
Clean version of #1954 .
UPDATED: I'd like to push ahead with this instance, and others, but I'm now starting to worry about where they should live:
Algebra.Bundles.Free.X or Algebra.Free.X? or somewhere else?
Many thanks for all the very helpful and constructive review suggestions, esp. wrt use of private modules. I thinkthat I shouldn't try to add any more to this for now.
UPDATED: now added use of Identity and Composition for MagmaHomomorphisms.
@MatthewDaggitt
Definitely prefer
Algebra.Free.X
I agree, and moved things accordingly.
Hmm I'm a little bit unsure of all these complicated named and unnamed submodules. Generally when they appear it means we haven't got the organisation quite right. It also makes it harder for the user to understand what's in scope at any given point in time.
I wonder how we can simplify it? While doing so we should consider how the organisation will be extended when encoding the free variants of more complicated structures.
So... I agree. I think (and hope!) that the use of private modules, and reverting to a more standard naming scheme, now means that the scoping is (much) easier to grasp.
But as for the use of nested modules in general, I personally do find it easier to use them to help localise/focus my thinking. And since the constructions are, categorically, unique 'up to', I've definitely found it helpful to keep the various appeals to Existence and Uniqueness separate, and local.
Regarding other instances of LeftAdjoint/Free constructions (I agree that we don't have good naming conventions for functorial constructions /constructions defined on functors in the library), I've also been experimenting with Church-style, level-raising versions. Now I'm undecided as to the best way to proceed: (more or less...)
FreeMagma (X : Setoid) = (M : Magma {c} {l}) (open Magma M) -> (X ⇒ setoid) -> setoid
etc. compared to explicitly constructing the syntax and equational theory presentation. Thoughts?
Re: merge going wrong. yes, but how? This was fine, for a good while... and hasn't changed, so what has? Did the merge of #1936 go wrong in some way? I'm not skilled in git bisect, or git blame so not sure how to proceed.
UPDATED: attempt at a fix. Let the tests decide!
Converting to DRAFT as a way of avoiding having to think about the CHANGELOG merge conflicts for the time being, until after v2.0 finally gets merged/released.
UPDATED: hopefully the PR is now ready for review after fixing up post-v2.0 merge conflicts plus some cosmetic fixes.
As stand-alone code, this is great.
But this also represents a non-trivial new design, and there's various things I am not so sure about. I don't want to merge this in right now, just to have a backwards compatibility problem in 3 months from now.
In places, this code seems really quite verbose (and that might be inevitable). And it might benefit quite a lot from the vapourware of a merge of parts of agda-categories into stdlib. And shrink too.
So I don't feel like pushing the 'merge' button. I wouldn't be upset of someone else did - I just don't want to be the one to commit this design to the library!
I'll wait until the discussion concludes on whether to merge at all, and then fix up whatever CHANGELOG conflicts there are at that point.
UPDATED: That said, if not merged (or, in any case!?), then it's probably worth lifting out those commits defining the Bundled Homomorphism constructions as a separate PR addressing #1960 ... see #2383
OK, a year has gone by, and even the one positive review is... unclear whether this should be merged.
I think it's worth pulling out the bundled Homomorphism commits, and trying to get those merged, ahead of returning to this one... but when? May 2025? :-(
I agree that splitting off the immediately mergable stuff into a separate PR is a good idea. As to the rest, you'll need to explicitly prod some not-me reviewers into action.
Marking as blocked-by-issue until #2383 (and possibly others!?) get completed and merged... and a CHANGELOG merge conflict takes care of worrying about needing to review the rest... ;-)