Bundles for Algebra.*Homomorphism, and their algebra: Hom-'sets' for Algebra

[jamesmckinna]

[cf. #1962 where there's the beginnings of a possible design for this, so that I could properly define a left adjoint to the forgetful functor Magma -> Setoid, witnessed on objects by Magma.setoid, but not really properly on morphisms. ]

Algebra.Morphism.Structures defines all the properties eg isMagmaHomomorphism of being a MagmaHomomorphism, but there's nowhere (?) in stdlib where those properties are bundled with their morphisms between the underlying Setoids.

Correspondingly, identity and composition for such things are distributed between Relation.Binary.Morphism.Construct and Algebra.Morphism.Construct, and which again operate only on the underlying proofs of properties.

Proposal: we add actual bundled homomorphisms for all the algebraic Structures in the library, on a 'one structure, one module' basis, to which we also package the Identity and Composition structures. UPDATED: bundled homomorphisms now under Algebra.Morphism.Bundles, with their Identity and Composition now handled under Algebra.Morphism.Construct

Now, this may already all be done (nicely, better, ...?) in agda-categories, and if so, then a plea to merge in this stuff.

[Taneb]

I support this idea but not the concrete details. It's not currently done better in agda-categories, or indeed at all. I'm working on that on the agda-categories side but was just planning to use Data.Product

[Taneb]

I'm not convinced we should have one module per structure but not strongly against it. I'd be interested to hear your justification of that over one file with all the bundles in it, which matches closer what we do elsewhere in the algebra hierarchy

[jamesmckinna]

but was just planning to use Data.Product
Is this because all the bundling/unbundling gets to painful?

[Taneb]

but was just planning to use Data.Product
Is this because all the bundling/unbundling gets to painful?

No, it's simply because the bundles didn't exist. It works a little better with some subcategory machinery in agda-categories but it's still not a perfect match

[jamesmckinna]

Re: one module per one algebra vs. how it is currently done now:
I think I managed to get confused as to whether all the various instances of identity and compose would share the same namespace happily? But if so, then indeed, consistency with current practice demands such an approach.

[Taneb]

I'd certainly be happy to see some experimentation with the design here

[JacquesCarette]

Strongly agree with

Proposal: we add actual bundled homomorphisms for all the algebraic Structures in the library,

as I ended up having to define some of these myself in a current project.

While I'm a huge fan of small files and small modules, right now we should stay consistent with the rest of Algebra and produce another monster (sigh).

[jamesmckinna]

One (at least!) outstanding question: where should the bundled versions of Construct.Identity and Construct.Composition live?
Can/should they live in Algebra.Morphism.Construct.*, as bundles after the definitions of the structures, or somewhere else entirely?

[Taneb]

Might be worth comparing .e.g. https://agda.github.io/agda-stdlib/Function.Construct.Identity.html which puts them in the same file

[jamesmckinna]

PR #1962 now makes that choice, and deploys it towards the actual intended uses.
Proposal at the top now updated accordingly.

[jamesmckinna]

Should be closed by #1962, modulo merge conflict (arising from #1936?).
UPDATED: NB it seems as though, while I added the necessary stubs for the Bundles, and Identity and Composition constructions to that PR, the actual additions exist only for Magma... so a lot of boring boilerplate left to do... later ;-)
UPDATED: leaving this issue open, as #1962 only adds bundled MagmaHomomorphisms... maybe a task-list is needed for the rest?

[jamesmckinna]

Hom-Sets or Hom-Setoid`s?

Whatever the merits (or otherwise) of #1962 there's no consideration of the 'obvious' extensional equality on *Morphisms induced by the underlying Setoid structure on the Carriers, and a PR resolving this should probably add that functionality. But then does such material belong in Algebra.Morphism.Structures or in the proposed Algebra.Morphism.Bundles?

[JacquesCarette]

Since most of stdlib is now Setoid based, I think it would make sense to continue that way, and then specialize to propeq for convenience when strictness is wanted.

Let me suggest Algebra.Morphism.Equivalence as yet another alternative for notion of morphism 'equality'? The structures and the bundles are what is "inside" a morphism, while this is about something external, which is why I'm thinking it belongs in a different part of the namespace.

[jamesmckinna]

Agree re: Setoid vs. Propositional split... it'll take a bit for me to rethink cherry-picking the various bits of #1962 to begin again with this.

As for *.Equivalence... interesting food for thought!?