[ add ] left- and right- actions induced by a Magma homomorphism

[jamesmckinna]

A simple piece of 'infrastructure' for Algebra.

NB. used extensively (implicitly) in #2854 etc. cf. #2892 and #2350 .

Issues:

• need to sort out the re-exporting strategy, plus suitable renaming (NOW: DONE?)

[Taneb]

I think this is a good addition, but if these are getting reexported by the various variations of ring morphisms, they should be renamed ⟦_⟧+_ and _+⟦_⟧ (and we should also have ⟦_⟧*_ and _*⟦_⟧, and probably something for module and lattice homomorphisms)

[jamesmckinna]

I think this is a good addition, but if these are getting reexported by the various variations of ring morphisms, they should be renamed ⟦_⟧+_ and _+⟦_⟧ (and we should also have ⟦_⟧*_ and _*⟦_⟧, and probably something for module and lattice homomorphisms)

Latest commit adds some of these export renamings. More to follow later, or downstream... most of the multiplicative substructure isn't opened in Structures, and I'm not sure what is gained by trying to chase down client openings... but agree that Lattice and Module might/should benefit from these things as well.

UPDATED: added renamed exports for Lattice and Module morphisms; the multiplicative structure of ring-like morphisms doesn't actually seem ever to be opened in stdlib, so no renaming export changes needed, it would seem?

[Taneb]

Even if they're not currently opened, it might be worth opening them specifcally to export ⟦_⟧*_ and _*⟦_⟧?

[jamesmckinna]

Even if they're not currently opened, it might be worth opening them specifcally to export ⟦_⟧*_ and _*⟦_⟧?

Good suggestion! Incoming commits...

[JacquesCarette]

I'm not keen on this design.

[JacquesCarette]

Fairbairn threshold? Do we really gain anything by adding these synonyms? The code already says we lose a bit (via the need to add hiding).

Personally I think that IsMagmaHomomorphism should be more minimalistic, and we should also have accompanying "extra kit" modules that we can use when needed. I've partially refactored agda-categories in that direction. And, in that case, seriously shrank the size of .agdai files and load times. I don't expect such an effect for Magma-related stuff, but this more "kitchen-sink" design approach is exactly what made working with Monoidal Categories so heavy.