[Agda] A plea for Set:Set

[Samuel Bronson]

On Tue, May 13, 2008 at 3:43 PM, Nils Anders Danielsson
<nils.anders.danielsson at gmail.com> wrote:
>  The flag turns off the universe check when you define data types and
>  record types. However, Set1 still does not match Set.

What is the price for this?