[Agda] Impredicativity

Martin Escardo m.escardo at cs.bham.ac.uk
Wed Oct 10 10:55:25 CEST 2018


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


More information about the Agda mailing list