This is always good practice, but would be especially helpful for the UniMath maintainers to keep this synced with UniMath upstream issues — in particular, I would be happy to prepare a PR for #17 , but first I have to figure out how to build it as intended.