<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<p>I am listening. :-)</p>
<p>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.)<br>
</p>
<p>But I think Andy wrote an improved version?<br>
</p>
<p>Best,<br>
Martin<br>
</p>
<div class="moz-cite-prefix">On 23/02/2023 10:48, Andrew Pitts
wrote:<br>
</div>
<blockquote type="cite" cite="mid:DFC4BCC4-2436-469D-A200-A03505B5073F@cl.cam.ac.uk">
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/" moz-do-not-send="true" class="moz-txt-link-freetext">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/" moz-do-not-send="true" class="moz-txt-link-freetext">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
<a class="moz-txt-link-rfc2396E" href="mailto:nk480@cl.cam.ac.uk"><nk480@cl.cam.ac.uk></a> 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>
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</div>
</blockquote>
</div>
<br>
</div>
<br>
<fieldset class="moz-mime-attachment-header"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</body>
</html>