Max Zeuner

Everything looks good to me. Will it be possible that people request reviews from me, without me being able to merge PRs?

This looks cool and I'm also interested to see how this relates to groupoid truncation. Did you see that we have another relation on lists that gives you finite multisets...

Thanks for your recommendation. There is indeed an ongoing effort to add schemes or at least affine schemes to the library. The idea is to not only work without choice...

Thanks for your elaborations and pointers to relevant literature. I still don't understand the functorial approach well enough to be able to say whether it is completely constructive or not....

Maybe we could use something like `_$r_` for ring morphisms?

Should we put it in the `README`?

Nice, I actually moved the prove of `APath` outside of the `where` block as well but didn't use `commAlgebraFromCommRing` in #929 (see diff [here](https://github.com/agda/cubical/pull/929/files#diff-98faa58f8c9d8a08689393b86fc64666ae13b667f58c78870def606175a3e21e)). Do you think it makes any...