<html xmlns:v="urn:schemas-microsoft-com:vml" 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=utf-8">
<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;}
/* List Definitions */
@list l0
{mso-list-id:1627003112;
mso-list-template-ids:-2065686686;}
@list l0:level1
{mso-level-start-at:2;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;}
@list l1
{mso-list-id:1664776063;
mso-list-template-ids:166521332;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-CA" link="blue" vlink="purple" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black">ℕ is well-ordered, so you may as well take the smallest i, not just ‘some’ i. If you further make your P i’s contractible (so as to be proof-irrelevant), then
you’re closer to the classical case.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black">In general, you might want to read everything under Relation.Binary.Indexed in the standard library. I much prefer the Homogeneous case, the Heterogeneous version
is weird in MLTT. [It’s not weird in other type theories.]<o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black">Jacques</span><span style="mso-fareast-language:EN-US"><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-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span lang="EN-US">From:</span></b><span lang="EN-US"> Agda <agda-bounces@lists.chalmers.se>
<b>On Behalf Of </b>Jason Hu<br>
<b>Sent:</b> November 12, 2021 9:49 AM<br>
<b>To:</b> agda@lists.chalmers.se<br>
<b>Subject:</b> [Agda] taking limit of a cumulative predicate<o:p></o:p></span></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<p class="MsoNormal" style="background:white"><span style="font-size:12.0pt;color:black">Hi all,<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span style="font-size:12.0pt;color:black">I bumped into a difference between type theory and set theory that I am somewhat struggling with in Agda.<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span style="font-size:12.0pt;color:black">Consider a type D and its predicate indexed by natural number:<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span style="font-size:12.0pt;color:black">P :
</span><span style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black">ℕ</span><span style="font-size:12.0pt;color:black"> → D → Set<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span style="font-size:12.0pt;color:black">where for x : D, P i x means x is in the subset of D described by P i.<o:p></o:p></span></p>
</div>
<div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black">Now imagine P is cumulative, namely<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black">cumu : </span><span style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black">∀</span><span style="font-size:12.0pt;color:black"> {i a} → P i a → P (suc i) a<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black">then sometimes, in set theory, we would conveniently take this index i to be \infty or omega and claim that such a subset is well-defined.
<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black">As you might have already noticed, this notion of taking a limit is difficult to formalize in a type theory. I can think of two tentative solutions:<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<ol start="1" type="1">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l1 level1 lfo1">
<span style="font-size:12.0pt">using Sigma type<o:p></o:p></span></li><li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l1 level1 lfo1">
<span style="font-size:12.0pt"><o:p> </o:p></span></li><li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l1 level1 lfo1">
<span style="font-size:12.0pt">P∞ x = </span><span style="font-size:12.0pt;font-family:"Cambria Math",serif">∃</span><span style="font-size:12.0pt"> λ i → P i x<o:p></o:p></span></li><li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l1 level1 lfo1">
<span style="font-size:12.0pt"><o:p> </o:p></span></li><li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l1 level1 lfo1">
<span style="font-size:12.0pt">This seems plausible, especially when we see this notion captures the fact that the set theoretic counterpart does implies for every P∞ x some index i exists. However, a problem arises when we encounter two instances of P∞ x.
Then to use them, we must unpack them, and now we have two distinct indices with no explicit relation. Meanwhile in set theory, we actually disregard the difference of indices, because we are talking about infinity.
<o:p></o:p></span></li></ol>
<ol start="2" type="1">
<li class="MsoNormal" style="color:black;mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;mso-list:l0 level1 lfo2">
<span style="font-size:12.0pt">another tentative solution is to redefine P such that it takes Maybe
</span><span style="font-size:12.0pt;font-family:"Cambria Math",serif">ℕ</span><span style="font-size:12.0pt"> and the nothing case represents infinity. But this solution has a big problem. There could be an x : D such that only (P nothing x) holds. In other
words, P becomes larger than the limit of its set theoretic counterpart.<o:p></o:p></span></li></ol>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black">Is there any solution to this problem which encodes the set theoretic notion more faithfully?<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div id="Signature">
<div>
<div id="divtagdefaultwrapper">
<p class="MsoNormal"><b><span style="font-size:12.0pt;color:black">Thanks,</span></b><span style="font-size:12.0pt;color:black"><o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><b><span style="font-size:12.0pt;color:black">Jason Hu</span></b><span style="font-size:12.0pt;color:black"><o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><b><span style="font-size:12.0pt;color:black"><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></span></b><span style="font-size:12.0pt;color:black"><o:p></o:p></span></p>
</div>
</div>
</div>
</div>
</div>
</div>
</body>
</html>