[Agda] Impredicativity

[Simon Boulier]

On 10/10/2018 10:29, Jesper Cockx wrote:
>
> Changing the termination checker to remove this assumption would take
> some more work. Would you be happy with a version of
> --impredicative-prop which is essentially a limited version of
> --type-in-type (and is thus unsound)?
>
Ho I see. For me it would be enough for experimentation. But people
should be aware that it does not turn Agda into a proof assistant for an
impredicative type theory.

Maybe we could name such a flag "--unsafe-impredicative-prop" ?