<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-2022-jp">
</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>Hi Timothy,</div>
<div><br>
</div>
<div>in this case there is no need for impredicativity. In fact you can define an equality of types which doesn$B!G(Bt increase the level:</div>
<div><br>
</div>
<div>
<div>data _$B"a(BT_ {a} (A : Set a) : Set a $B"*(B Set a where</div>
<div> refl : A $B"a(BT A</div>
</div>
<div><br>
</div>
<div>And this is equivalent to the usual equality only on a lower level. </div>
<div><br>
</div>
<div>Actually the view that equality of types is a type (of the same level) is supported by Univalent Type Theory which assumes that equality of types is equivalent to equivalence which is a type at the same level.</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>Timothy Carstens <<a href="mailto:intoverflow@gmail.com">intoverflow@gmail.com</a>><br>
<span style="font-weight:bold">Date: </span>Wednesday, 30 December 2015 04:13<br>
<span style="font-weight:bold">To: </span>Thorsten Altenkirch <<a href="mailto:thorsten.altenkirch@nottingham.ac.uk">thorsten.altenkirch@nottingham.ac.uk</a>><br>
<span style="font-weight:bold">Cc: </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>Re: [Agda] Why no impredicative prop?<br>
</div>
<div><br>
</div>
<div>
<div>
<div dir="ltr">Forgive me, I errored in my description of the issue.
<div><br>
</div>
<div>In their example they define ref : type -> type, but the definition witnesses an equality over type, which pushes ref into Set (i + 1).</div>
<div><br>
</div>
<div>-t<br>
</div>
<div><br>
</div>
</div>
<div class="gmail_extra"><br>
<div class="gmail_quote">On Tue, Dec 29, 2015 at 7:13 PM, Timothy Carstens <span dir="ltr">
<<a href="mailto:intoverflow@gmail.com" target="_blank">intoverflow@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">For most of the work I've done I haven't needed an impredicative universe; that is, the main reason I'd use Prop in Coq was that the OCaml extractor would eliminate Prop terms, which was nice.
<div><br>
</div>
<div>But then I tried to implement indirection theory in the style of Hobor, Dockins, Appel [1]. One can carry out their construction just fine, but (from what I can tell) using the construction in the manner shown in their examples requires an impredicative
sort.</div>
<div><br>
</div>
<div>Namely, in section 4.1 they wind up in a situation where they have</div>
<div><br>
</div>
<div>T some type, say Set i</div>
<div><br>
</div>
<div>type = memtype * value -> T</div>
<div><br>
</div>
<div>ref : type -> type</div>
<div><br>
</div>
<div>At this point, their usage of 'ref' seems to require (type -> type : T), which only seems possible if T is impredicative.</div>
<div><br>
</div>
<div>I'm unsure whether or not their construction could be carried out in a satisfactory way by (for example) trying to make a universe-polymoprhic version of 'type'. Regardless, running into this obstacle got me to wondering whether or not there was a theoretical
obstruction to Agda having an impredicative prop.</div>
<div><br>
</div>
<div>[1] <a href="http://vst.cs.princeton.edu/msl/indirection.pdf" target="_blank">http://vst.cs.princeton.edu/msl/indirection.pdf</a></div>
<span class="HOEnZb"><font color="#888888">
<div><br>
</div>
<div>-t</div>
<div><br>
</div>
</font></span></div>
<div class="HOEnZb">
<div class="h5">
<div class="gmail_extra"><br>
<div class="gmail_quote">On Tue, Dec 29, 2015 at 2:11 PM, Thorsten Altenkirch <span dir="ltr">
<<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk" target="_blank">Thorsten.Altenkirch@nottingham.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word;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$B!G(Bt know an intuitionistic justification of impredicativity.</div>
<div><br>
</div>
<div>Thorsten</div>
<div><br>
</div>
<span>
<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" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Timothy Carstens <<a href="mailto:intoverflow@gmail.com" target="_blank">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" target="_blank">agda@lists.chalmers.se</a>" <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<span style="font-weight:bold">Subject: </span>[Agda] Why no impredicative prop?<br>
</div>
<div>
<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>
</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>
</div>
</blockquote>
</div>
<br>
</div>
</div>
</div>
</blockquote>
</div>
<br>
</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>