Add bundled homomorphisms

[jamesmckinna]

Cherry-picked and enhanced from #1962 . Fixes #1960 .

TODO:

• the Algebra.Morphism.Construct.{Identity|Composition} material
• RingWithoutOne doesn't appear to export its own Raw substructure, so that should be added? ditto. KleeneAlgebra
• homomorphisms for all the existing Structures/Bundles

NB

• doesn't address the Setoid structure on Homs at all... (brain-fade; sigh)
• for bundles which export two sub-bundles, usual 'diamond' problem about re-opening those publicly for export, so someone with a good eye for such things,... please nitpick those details!
• UPDATED: Semiring and Ring homomorphisms should export a SuccessorSetHomomorphism structure/bundle
  only after going back to Literals for any ring? #1363 through the medium of (the initial) SuccessorSet and its consequences for Algebra.Structures having (Is)SuccessorSet fields...

[Taneb]

Before I look at this at all I just want to say thanks for tackling it! I've been avoiding it with the hope that we can get a solution for #2287, but that looks a long way off.

[jamesmckinna]

@Taneb Indeed! This kind of boilerplate-bashing is quite fatiguing, until you run up against the 'diamond' re-export problem, at which point my powers fail me in different ways, trying to work out what should get re-exported from where... plus discovering that (still!) not everything is present which perhaps ought to be... ;-)

UPDATED: moving to DRAFT until I have time to finish off (some of) the outstanding items above.

[JacquesCarette]

This all seems quite reasonable. I am doing this as a comment because it seems incomplete - but I have no specific improvement that I'd like to see in the code that is here.

[jamesmckinna]

@JacquesCarette @Taneb I have now added the 'missing' parts of the PR (as in the revised opening preamble above), and so (hopefully) now stopping there...

[Taneb]

The following don't need changes now but we should make issues for them so we don't lose track:

• Bundles for monomorphisms and isomorphisms (and epimorphisms if we add those) Add bundled mono-/iso-{/epi-} morphisms #2387
• Bundles for lattice-like and module-like morphisms Add bundles for lattice-like and module-like morphisms #2388

[jamesmckinna]

Currently badged as v2.2, but could merge for v2.1?

[jamesmckinna]

Have now updated the CHANGELOG for v2.2, but there is still the unresolved discussion above about Identity and Composition apparently needing to take full bundles in order to get the correct setoid properties refl and trans... or should these be supplied explicitly?

UPDATED: pending resolution of this issue, PR is now up-to-date and ready-to-merge. @MatthewDaggitt are you happy that your review comments have been addressed?

[MatthewDaggitt]

I think it's fine that they take the full bundles for now.