opposite of a `Ring` [clean version of pr #1900]#1910

MatthewDaggitt merged 8 commits intoagda:masteragda/agda-stdlib:masterfrom

jamesmckinna:ring-cleanjamesmckinna/agda-stdlib:ring-cleanCopy head branch name to clipboard