<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">

<head>

<meta http-equiv="Content-Type" content="text/html; charset=ks_c_5601-1987">

<meta name="Generator" content="Microsoft Word 15 (filtered medium)">

<style><!--

/* Font Definitions */

@font-face

        {font-family:"Cambria Math";

        panose-1:2 4 5 3 5 4 6 3 2 4;}

@font-face

        {font-family:Calibri;

        panose-1:2 15 5 2 2 2 4 3 2 4;}

/* Style Definitions */

p.MsoNormal, li.MsoNormal, div.MsoNormal

        {margin:0cm;

        font-size:11.0pt;

        font-family:"Calibri",sans-serif;}

a:link, span.MsoHyperlink

        {mso-style-priority:99;

        color:blue;

        text-decoration:underline;}

span.EmailStyle19

        {mso-style-type:personal-reply;

        font-family:"Calibri",sans-serif;

        color:windowtext;}

.MsoChpDefault

        {mso-style-type:export-only;

        font-size:10.0pt;}

@page WordSection1

        {size:612.0pt 792.0pt;

        margin:72.0pt 72.0pt 72.0pt 72.0pt;}

div.WordSection1

        {page:WordSection1;}

--></style>

</head>

<body lang="EN-GB" link="blue" vlink="purple" style="word-wrap:break-word">

<div class="WordSection1">

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">One way to add an impredicative universe on Set is<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">{-# NO_UNIVERSE_CHECK #-}<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">record Pi {ЇЄ} (A : Set ЇЄ)(B : A Ёц Set)  : Set where<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">  constructor lam<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">  field<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">    _$_ : (a : A) Ёц B a<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">  infixl 10 _$_<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">  <o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">open Pi<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">syntax Pi A (Ѕы x Ёц P)  = Ѕа[ x

</span><span style="font-family:"Cambria Math",serif;mso-fareast-language:EN-US">Ёє</span><span style="mso-fareast-language:EN-US"> A ] P<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">syntax lam (Ѕы x Ёц p) = Ѕы[ x ] p<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US">but the syntax is a bit ugly. Also I am not sure whether this works for Prop.<o:p></o:p></span></p>

<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>

<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">

<p class="MsoNormal" style="margin-bottom:12.0pt"><b><span style="font-size:12.0pt;color:black">From:

</span></b><span style="font-size:12.0pt;color:black">Agda <agda-bounces@lists.chalmers.se> on behalf of Neel Krishnaswami <nk480@cl.cam.ac.uk><br>

<b>Date: </b>Thursday, 23 February 2023 at 09:47<br>

<b>To: </b>Agda mailing list <agda@lists.chalmers.se><br>

<b>Subject: </b>[Agda] Impredicative prop?<o:p></o:p></span></p>

</div>

<div>

<p class="MsoNormal">Hi,<br>

<br>

I'd like to teach a course next year which (among other things) proves a <br>

simple termination result for System F in Agda.<br>

<br>

Obviously, I can't do this without an impredicative Prop sort, and so I <br>

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 <br>

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>

<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><o:p></o:p></p>

</div>

</div>

<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 contact the sender and delete the email and

attachment. 

Any views or opinions expressed by the author of this email do not

necessarily reflect the views of the University of Nottingham. Email

communications with the University of Nottingham may be monitored 

where permitted by law.

</PRE></body>

</html>