<html><head><meta http-equiv="content-type" content="text/html; charset=us-ascii"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">This makes me think of the work Martin Escardo did around 2015. Martin can speak for himself if he is listening, but see here<div><br></div><div><a href="https://www.cs.bham.ac.uk/~mhe/impredicativity/">https://www.cs.bham.ac.uk/~mhe/impredicativity/</a></div><div><br></div><div>and here</div><div><br></div><div><a href="https://www.cs.bham.ac.uk/~mhe/impredicativity-via-rewriting/">https://www.cs.bham.ac.uk/~mhe/impredicativity-via-rewriting/</a></div><div><br></div><div>Andy</div><div><br><div><br><blockquote type="cite"><div>On 23 Feb 2023, at 09:46, Neel Krishnaswami <nk480@cl.cam.ac.uk> wrote:</div><br class="Apple-interchange-newline"><div><div>Hi,<br><br>I'd like to teach a course next year which (among other things) proves a simple termination result for System F in Agda.<br><br>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.<br><br>As far as I can tell, there are two things which would need to be done:<br><br>1. Turn off universe levels for Prop.<br>2. Enforce the strict positivity restriction on Prop-valued datatype declarations.<br><br>Is there anything I'm missing?<br><br>Thanks,<br>Neel<br><br>_______________________________________________<br>Agda mailing list<br>Agda@lists.chalmers.se<br>https://lists.chalmers.se/mailman/listinfo/agda<br></div></div></blockquote></div><br></div></body></html>