On 2020-01-22 16:34, Mathijs Kwik wrote: > Neither the manual nor the release notes make note of this facility. It has not been released yet. > Why not just make the default version in Data.Empty use irrelevance? "Redefine Bottom to make use of Prop?" https://github.com/agda/agda-stdlib/issues/645 -- /NAD