Felix Cherubini

Put on hold, since it uses flat in a way that is not supported by the latest master of agda.

This is mostly solved by #585. More precisely, the feature as requested above works, if the variables for the ring solver are introduced after all other variables. The remaining problem...

I'll do 1 3 by: * Constructing algebra structure on the list-polynomials * Show the map from the universal property of the polynomial HiT in Algebra.CommAlgebra.FreeCommAlgebra is surjective * ......

Or maybe I don't - just realized I have to show, that the inverse to the induced morphism is an algebra-hom... So it might still be easier to just show...

Just in case this is still relevant for anyone: This warning can be irgnored and it doesn't come up, if you check the library with Agda 2.6.2 -- which is...

Maybe we could also say: If your PR is not assigned to someone in a couple of days, assign it to one of the reviewers..

Maybe that's a good overview, of the things to review: https://github.com/agda/cubical/pulls?q=is%3Apr+is%3Aopen+sort%3Aupdated-asc+draft%3Afalse

Done with merging of the PR

I agree that there is some inconsistency among Group and AbGroup. I would be more for moving things away from Base in AbGroup. According to *my personal taste* Polynomials should...

> For each algebraic structure `S` I would suggest the following organization: > > * `Base.agda` : definition and basic operation of `S`, maybe some basic equivalence (like SIP instance...