<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=ks_c_5601-1987">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
I don't think so, though. Level should just be a counter for the universes, so it doesn't have to be big.</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<span style="font-family: "Courier New", monospace;">open import Level</span><span></span><br>
<div><span style="font-family: "Courier New", monospace;">Foo : Set</span><br>
</div>
<span style="font-family: "Courier New", monospace;">Foo = Level</span><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
This code actually works in Agda. <br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a target="_blank"></a></b></span></span></font> </div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Stefan Monnier <monnier@iro.umontreal.ca><br>
<b>Sent:</b> March 10, 2019 2:18 PM<br>
<b>To:</b> agda@lists.chalmers.se<br>
<b>Subject:</b> Re: [Agda] Proving equality of levels with heterogeneous equality.</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">> It's not possible to prove this in Agda because the pattern matching<br>
> unification algorithm only deals with data constructors (such as 'zero' or<br>
> 'suc'), not with type constructors (such as 'Nat' or 'Set'). I don't<br>
> immediately see if your particular lemma here would break soundness, but<br>
> that doesn't say much.<br>
<br>
I'm not surprised it's not possible, but I'm surprised by<br>
this explanation. I'd have thought the first reason is that<br>
<br>
§¤©û ¡Õ §¤©ü<br>
<br>
is ill-typed because<br>
<br>
§¤©û, §¤©ü : Level<br>
(¡Õ) : {§¤ : Level} ¡æ {A : Set §¤} ¡æ A ¡æ A ¡æ Set §¤<br>
<br>
and there is no §¤ for which `Level : Set §¤`<br>
<br>
<br>
Stefan<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><br>
</div>
</span></font></div>
</body>
</html>