We rename * to + in both ThGrp and ThAbGrp (which extends ThGrp with a commutativity axiom). With the present setup, it will not be the case that ThAddGrp will be a proper inclusion of ThAddAbGrp.
One way to address this is to make the data to rename ThGrp (resp. ThAbGrp) be the renaming morphism (as generated by the existing tooling) from ThMon to ThAddMon as well as an inclusion from ThMon into ThGrp (resp ThAbGrp). This fancier renaming function will make sure to use the fresh scopetags from ThAddMon in both ThAddGrp and ThAddAbGrp.
There are new features for renaming in the pipeline (https://github.com/AlgebraicJulia/GATlab.jl/pull/147 and https://github.com/AlgebraicJulia/GATlab.jl/pull/146) which suffer from a common problem of generating completely fresh ScopeTags for the renamed theory. Consider the following scenario:
We rename
*to+in bothThGrpandThAbGrp(which extendsThGrpwith a commutativity axiom). With the present setup, it will not be the case thatThAddGrpwill be a proper inclusion ofThAddAbGrp.One way to address this is to make the data to rename
ThGrp(resp.ThAbGrp) be the renaming morphism (as generated by the existing tooling) fromThMontoThAddMonas well as an inclusion fromThMonintoThGrp(respThAbGrp). This fancier renaming function will make sure to use the fresh scopetags fromThAddMonin bothThAddGrpandThAddAbGrp.