[Agda] Impredicative prop?

[Andrew Pitts]

This makes me think of the work Martin Escardo did around 2015. Martin can speak for himself if he is listening, but see here

https://www.cs.bham.ac.uk/~mhe/impredicativity/

and here

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

Andy


> On 23 Feb 2023, at 09:46, Neel Krishnaswami <nk480 at cl.cam.ac.uk> wrote:
> 
> 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
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20230223/26eaaeab/attachment-0001.html>