Follow up from [#1727](https://github.com/agda/agda-stdlib/pull/1727) and https://github.com/agda/agda-stdlib/issues/1493