[Agda] A plea for Set:Set

[Nils Anders Danielsson]

On Wed, May 14, 2008 at 12:26 AM, Samuel Bronson <naesten at gmail.com> wrote:
>
>  It doesn't seem to work:
>
>  /home/naesten/hacking/haskell/Agda2/examples/Rustle.agda:29,30-31
>  Set2 != Set1
>  when checking that the expression U has type Set

No, hence the "almost" in my previous reply to Thorsten.

If you really want to implement Hurken's paradox you should wrap
something in a data type. (A : Set) -> A -> A has type Set1, but

  data T : Set where
    t : ((A : Set) -> A -> A) -> T

works (using --no-universe-check).

-- 
/NAD