Proofs that identity and composition of homomorphisms are homomorphisms

[Taneb]

I'd like there to be modules (maybe Algebra.Morphism.Construction.Identity and Algebra.Morphism.Construction.Composition but this is an unpainted bike shed) which have witnesses that the various things in Algebra.Morphism.Structures are satisfied by id and _∘_ from Function.Base.

I think this requires the algebraic structures to be the actual algebraic structure, not RawX

[MatthewDaggitt]

No objections from me (apart from Construction -> Construct). We already have such modules for morphisms between binary relations:

https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/Morphism/Construct/Composition.agda
https://github.com/agda/agda-stdlib/blob/master/src/Relation/Binary/Morphism/Construct/Identity.agda