[Agda] Impredicative prop?

[Martin Escardo]

I am listening. :-)

Yes, I did that for Andy who at some point needed a small type of 
propositions. I am not sure it still works in the current version of 
Agda. (I think also Andreas and/or Jesper improved rewriting for the 
purposes of the second file, at that time.)

But I think Andy wrote an improved version?

Best,
Martin

On 23/02/2023 10:48, Andrew Pitts wrote:
> 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
>
>
> _______________________________________________
> 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/72be8fd0/attachment.html>