<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=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:DengXian;
panose-1:2 1 6 0 3 1 1 1 1 1;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"\@DengXian";
panose-1:2 1 6 0 3 1 1 1 1 1;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
.MsoChpDefault
{mso-style-type:export-only;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.25in 1.0in 1.25in;}
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:.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level2
{mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level3
{mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level4
{mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level5
{mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level6
{mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level7
{mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level8
{mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l0:level9
{mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l1
{mso-list-id:1664776063;
mso-list-template-ids:166521332;}
@list l1:level1
{mso-level-tab-stop:.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l1:level2
{mso-level-tab-stop:1.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l1:level3
{mso-level-tab-stop:1.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l1:level4
{mso-level-tab-stop:2.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l1:level5
{mso-level-tab-stop:2.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l1:level6
{mso-level-tab-stop:3.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l1:level7
{mso-level-tab-stop:3.5in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l1:level8
{mso-level-tab-stop:4.0in;
mso-level-number-position:left;
text-indent:-.25in;}
@list l1:level9
{mso-level-tab-stop:4.5in;
mso-level-number-position:left;
text-indent:-.25in;}
ol
{margin-bottom:0in;}
ul
{margin-bottom:0in;}
--></style>
</head>
<body lang="EN-US" link="blue" vlink="#954F72" style="word-wrap:break-word">
<div class="WordSection1">
<p class="MsoNormal">Hmmmm, if P is irrelevant, then in fact the Sigma type solution would seem to workout. Now in my code P is irrelevant up to my usage, so I am experimenting and see if Sigma suffices.</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">you also seem to suggest</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">P<span lang="ZH-CN" style="font-family:DengXian">∞</span> x =
<span style="font-family:"Cambria Math",serif">∃</span> λ i <span lang="ZH-CN" style="font-family:DengXian">
→</span> P i x × <span style="font-family:"Cambria Math",serif">∀</span> {j} <span lang="ZH-CN" style="font-family:DengXian">
→</span> P j x <span lang="ZH-CN" style="font-family:DengXian">→</span> i <span lang="ZH-CN" style="font-family:DengXian">
≤</span> j</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">That is, the hidden I is the smallest one. This is quite plausible actually. But I can imagine there will be problems proving subsumption of limit:</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">subsum : <span style="font-family:"Cambria Math",serif">∀</span> {i x}
<span lang="ZH-CN" style="font-family:DengXian">→</span> P i x <span lang="ZH-CN" style="font-family:DengXian">
→</span> P<span lang="ZH-CN" style="font-family:DengXian">∞</span> x</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">I suppose this exposes another difference between type theory and set theory. In set theory, we somewhat get this for free: we morally have an oracle (possibly with the power of Choice) which gives you the smallest j such that P j x holds
and this j is hidden in an existential quantifier. However, in type theory, we must explicitly solve this j, but might not always be possible.
</p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
<p class="MsoNormal">Jason Hu<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="mso-element:para-border-div;border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal" style="border:none;padding:0in"><b>From: </b><a href="mailto:carette@mcmaster.ca">Carette, Jacques</a><br>
<b>Sent: </b>Friday, November 12, 2021 1:03 PM<br>
<b>To: </b><a href="mailto:fdhzs2010@hotmail.com">Jason Hu</a>; <a href="mailto:agda@lists.chalmers.se">
agda@lists.chalmers.se</a><br>
<b>Subject: </b>RE: taking limit of a cumulative predicate</p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><span lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black"><o:p> </o:p></span></p>
<p class="MsoNormal"><span lang="EN-CA" style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black">Jacques</span><span lang="EN-CA" style="mso-fareast-language:EN-US"><o:p></o:p></span></p>
<p class="MsoNormal"><span lang="EN-CA" style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0in 0in 0in 4.0pt">
<div>
<div style="border:none;border-top:solid #E1E1E1 1.0pt;padding:3.0pt 0in 0in 0in">
<p class="MsoNormal"><b>From:</b> 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></p>
</div>
</div>
<p class="MsoNormal"><span lang="EN-CA"><o:p> </o:p></span></p>
<div>
<p class="MsoNormal" style="background:white"><span lang="EN-CA" style="font-size:12.0pt;color:black">Hi all,<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span lang="EN-CA" style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span lang="EN-CA" style="font-size:12.0pt;color:black">P :
</span><span lang="EN-CA" style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black">ℕ</span><span lang="EN-CA" style="font-size:12.0pt;color:black"> → D → Set<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span lang="EN-CA" style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="background:white"><span lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span lang="EN-CA" style="font-size:12.0pt;color:black">cumu :
</span><span lang="EN-CA" style="font-size:12.0pt;font-family:"Cambria Math",serif;color:black">∀</span><span lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt;color:black"><o:p> </o:p></span></p>
</div>
<div>
<p class="MsoNormal"><span lang="EN-CA" 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 lang="EN-CA" 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 lang="EN-CA" 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 lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt">P∞ x = </span><span lang="EN-CA" style="font-size:12.0pt;font-family:"Cambria Math",serif">∃</span><span lang="EN-CA" 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 lang="EN-CA" 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 lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt">another tentative solution is to redefine P such that it takes Maybe
</span><span lang="EN-CA" style="font-size:12.0pt;font-family:"Cambria Math",serif">ℕ</span><span lang="EN-CA" 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 lang="EN-CA" 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 lang="EN-CA" 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 lang="EN-CA" style="font-size:12.0pt;color:black">Thanks,</span></b><span lang="EN-CA" style="font-size:12.0pt;color:black"><o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><b><span lang="EN-CA" style="font-size:12.0pt;color:black">Jason Hu</span></b><span lang="EN-CA" style="font-size:12.0pt;color:black"><o:p></o:p></span></p>
</div>
</div>
</div>
</div>
</div>
<p class="MsoNormal"><b><span lang="EN-CA" style="font-size:12.0pt;color:black"><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></span></b><span lang="EN-CA" style="font-size:12.0pt;color:black"><o:p></o:p></span></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>