Adding explicit zero algebras

[djspacewhale]

Added initial work for the zero ring and zero abelian group, along with proofs of their uniqueness up to contractible type. Remaining work is refactoring for the rest of the zero algebras along the way and the final uniqueness proof by SIP.

[EgbertRijke]

Awesome! Thanks for contributing to agda-unimath!

[fredrik-bakke]

It would be nice to have these changes merged soon, but we have suggested some changes that need to be addressed first. What is your status, @djspacewhale? If you prefer, I can take care of the finishing touches for you and merge this.

[djspacewhale]

Sorry for disappearing for a while there. I'll merge these today.

[fredrik-bakke]

Oh, judging from the "checks" below, it seems either one of your files is missing an import, or is-contr-subgroup-is-trivial-Group is called something else. Also, you will have to run our pre-commit hooks on your project to apply auto-formatting rules.

For a guide on how to set up pre-commit, see here:

• https://unimath.github.io/agda-unimath/HOWTO-INSTALL.html#contributor-setup

To learn more about what it does, see here:

• https://unimath.github.io/agda-unimath/CONTRIBUTING.html

[fredrik-bakke]

Let me know if you have any questions!

[fredrik-bakke]

Excellent! I will enable auto-merging now