Generate homomorphism types for algebraic structures

Stream: general

[Fabian Glöckle]

Hello everyone,
I have finally cleaned up the code for auto-generating homomorphism types for algebraic structures.
The idea is that for structures like monoid, group, ring, ..., the type of homomorphisms can simply be read from the definition: morphisms need to be "compatible with all operations".
The code linked below generates the structure of homomorphisms and the lemmas that compositions of homomorphisms and identities are homomorphisms, and defines the concrete_category belonging to the structure.
Moreover, it defines forgetful functors, whenever one structure is an extension of another (in the sense of also having its fields), and the respective instances.
Below the code there is a brief section of examples, also listing current restrictions (e.g. only "old style" structures).
https://github.com/faabian/mathlib/blob/3.5/meta.lean
I think this is relevant because, as pointed out by @Johan Commelin and others, currently the library does not reflect the link between a class of objects and its (manually defined) homomorphism type.
A goal might be to create a "table" linking structures to their manually defined homomorphism types (e. g. for topological spaces) and to auto-generate the ones for structures derived from these (e. g. topological groups).

[Kevin Buzzard]

Does it need Lean 3.5?

[Johan Commelin]

I think that in the end it does not.

[Fabian Glöckle]

No it doesn't, structure declarations are now made with emit_code_here, not the Lean 3.5 interface