<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Hi, Thorsten.<div class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Dec 29, 2015, at 5:11 PM, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" class="">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:</div><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; font-size: 14px; font-family: Calibri, sans-serif;" class="">
<div class=""><br class="">
</div>
<div class="">More on the philosphical side: impredicativity is basically a classical idea which arises from the identification of Prop and Bool. I don’t know an intuitionistic justification of impredicativity.</div></div></div></blockquote><div><br class=""></div><div>I am not sure I understand what this means. Do you have a reference regarding this? System F is intuitionistic, but doesn’t this claim it isn’t?</div><div><br class=""></div><div>Very best,</div><div>Harley</div><br class=""><blockquote type="cite" class=""><div class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; font-size: 14px; font-family: Calibri, sans-serif;" class="">
<div class=""><br class="">
</div>
<div class="">Thorsten</div>
<div class=""><br class="">
</div>
<span id="OLK_SRC_BODY_SECTION" class="">
<div style="font-family: Calibri; font-size: 11pt; text-align: left; border-width: 1pt medium medium; border-style: solid none none; padding: 3pt 0in 0in; border-top-color: rgb(181, 196, 223);" class="">
<span style="font-weight:bold" class="">From: </span><<a href="mailto:agda-bounces@lists.chalmers.se" class="">agda-bounces@lists.chalmers.se</a>> on behalf of Timothy Carstens <<a href="mailto:intoverflow@gmail.com" class="">intoverflow@gmail.com</a>><br class="">
<span style="font-weight:bold" class="">Date: </span>Tuesday, 29 December 2015 17:19<br class="">
<span style="font-weight:bold" class="">To: </span>"<a href="mailto:agda@lists.chalmers.se" class="">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se" class="">agda@lists.chalmers.se</a>><br class="">
<span style="font-weight:bold" class="">Subject: </span>[Agda] Why no impredicative prop?<br class="">
</div>
<div class=""><br class="">
</div>
<div class="">
<div class="">
<div dir="ltr" class="">
<div class="">Hello,</div>
<div class=""><br class="">
</div>
<div class="">I'm a relatively new Agda user, coming from a background using Coq for the past few years. As is well known, Coq has an impredicative Prop sort, while Agda does not.</div>
<div class=""><br class="">
</div>
<div class="">Why not? Is it simply a matter of project goals, or is there something about Agda's underlying theory which is incompatible with having an impredicative sort at the bottom of the universe hierarchy?</div>
<div class=""><br class="">
</div>
<div class="">Forgive me if this is an old topic or has an obvious answer; I'm not a logician, but I use proof assistants at work.<br class="">
</div>
<div class="">-t</div>
<div class=""><br class="">
</div>
</div>
</div>
</div>
</span>
<pre class="">
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it.
Please do not use, copy or disclose the information contained in this
message or in any attachment. Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.
This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.
</pre></div>
_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></div></body></html>