<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; color: rgb(0, 0, 0); font-size: 14px; font-family: Calibri, sans-serif;">
<div>Actually why do you need an impredicative universe?</div>
<div><br>
</div>
<div>From a purely pragmatic point it is a bit strange if one universe behaves different from the other one. But having two impredicative universes is already unsound.</div>
<div><br>
</div>
<div>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><br>
</div>
<div>Thorsten</div>
<div><br>
</div>
<span id="OLK_SRC_BODY_SECTION">
<div style="font-family:Calibri; font-size:11pt; text-align:left; color:black; BORDER-BOTTOM: medium none; BORDER-LEFT: medium none; PADDING-BOTTOM: 0in; PADDING-LEFT: 0in; PADDING-RIGHT: 0in; BORDER-TOP: #b5c4df 1pt solid; BORDER-RIGHT: medium none; PADDING-TOP: 3pt">
<span style="font-weight:bold">From: </span><<a href="mailto:agda-bounces@lists.chalmers.se">agda-bounces@lists.chalmers.se</a>> on behalf of Timothy Carstens <<a href="mailto:intoverflow@gmail.com">intoverflow@gmail.com</a>><br>
<span style="font-weight:bold">Date: </span>Tuesday, 29 December 2015 17:19<br>
<span style="font-weight:bold">To: </span>"<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br>
<span style="font-weight:bold">Subject: </span>[Agda] Why no impredicative prop?<br>
</div>
<div><br>
</div>
<div>
<div>
<div dir="ltr">
<div>Hello,</div>
<div><br>
</div>
<div>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><br>
</div>
<div>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><br>
</div>
<div>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>
</div>
<div>-t</div>
<div><br>
</div>
</div>
</div>
</div>
</span>
<PRE>
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></body>
</html>