[Agda] Impredicative prop?

[Nils Anders Danielsson]

On 2023-02-23 10:46, Neel Krishnaswami wrote:
> 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?

Agda's termination checker is based on the assumption that the language
is predicative.

-- 
/NAD