[Agda] Impredicative prop?

[Neel Krishnaswami]

Hi,

I'd like to teach a course next year which (among other things) proves a 
simple termination result for System F in Agda.

Obviously, I can't do this without an impredicative Prop sort, and so I 
was wondering what changes would need to be made to Agda to support it.

As far as I can tell, there are two things which would need to be done:

1. Turn off universe levels for Prop.
2. Enforce the strict positivity restriction on Prop-valued datatype 
declarations.

Is there anything I'm missing?

Thanks,
Neel