[Agda] This ain't right, is it?

[Benja Fallenstein]

On Sat, Oct 31, 2009 at 1:18 AM, Dan Doel <dan.doel at gmail.com> wrote:
> Technically, this wouldn't be Set : Set. It'd be impredicativity if we still
> have:
>
>  Set i : Set (suc i)
...
> However, impredicativity leads to similar problems as Set : Set in all but the
> lowest level ...

Right... I'm trying to make a universe-polymorphic translation of an
impredicative library, so it's annoying if the typechecker does not
complain about impredicative things :-)

-b