[Agda] Impredicativity

[Martin Escardo]

There is also an alternative hack, using rewriting rather than 
--type-in-type:

http://www.cs.bham.ac.uk/~mhe/impredicativity-via-rewriting/

Martin

On 10/10/18 09:19, simon.boulier at ens-rennes.fr wrote:
> Hi all,
> 
> I need an impredicative Prop universe.
> 
> Would it be lot of work to add an experimental "--impredicative-prop" flag?
> 
> I am also aware of this hack of Martin Escardo:
> http://www.cs.bham.ac.uk/~mhe/impredicativity/
> But I am not sure to which extent I can adapt it to my needs...
> 
> Cheers,
> 
> 
> Simon
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe