[Agda] Impredicative prop?

[Andreas Nuyts]

Dear Neel,

I don't know the answer to your question, but as an alternative, you 
could modify System F to make it predicative:

Leivant, 1991, Finitely Stratified Polymorphism
https://www.sciencedirect.com/science/article/pii/0890540191900535

Best,
Andreas

On 23.02.23 10:46, Neel Krishnaswami 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