<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
</head>
<body>
<p>
<blockquote type="cite">
<pre style="white-space: pre-wrap; color: rgb(0, 0, 0); font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration-style: initial; text-decoration-color: initial;">Thanks for finding this. I guess this is in a longer tradition of
problems with the sized types implementation, see e.g.
<a href="https://github.com/agda/agda/issues/2820,">https://github.com/agda/agda/issues/2820,</a>
<a href="https://github.com/agda/agda/issues/3026,">https://github.com/agda/agda/issues/3026,</a>
<a href="https://github.com/agda/agda/issues/1428.">https://github.com/agda/agda/issues/1428.</a>
I don't understand whether it has overlap with existing issues. You
don't use the infinity size, nor equality. So maybe it's a new kind of
issue, coming from interaction of sizes with inductive types?
</pre>
</blockquote>
It is an elaboration on the bug about well-founded induction and
sized types (<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/3026">https://github.com/agda/agda/issues/3026</a>). The main
difference with the latter is that, instead of importing the
well-founded module of Agda's library, I am using an apparently
innocent definition of a sized inductive type :<br>
</p>
<p>data ℕ {s : Size} : Set where<br>
zero : ℕ<br>
suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}</p>
<p>as an accessibility predicate for the relation between sized
induced by the construction Size<. By using the
"size-elimproved" construction (also an elaboration of code found
here:
<a class="moz-txt-link-freetext" href="https://github.com/agda/agda/issues/2820#issuecomment-339969286">https://github.com/agda/agda/issues/2820#issuecomment-339969286</a>) I
can then define a "natural number" for each size, including
infinity (note that sizes are implicit arguments, so infinity does
not show up in the code, but it's there all right). For size =
infinity, the "natural number" </p>
<p>foo : ℕ<br>
foo = size-elimproved (λ s → ℕ{s}) (λ _ H → suc λ { {j} → H j } )
_</p>
<p>is easily shown to be a successor of itself, which the definition
of "natural numbers" forbids, hence the proof of False.</p>
<p>Overall, I'm not sure it's worth a new bug report, as it is an
elaboration of existing constructions. My main point in showing
this is that one may easily "believe" that one is defining natural
numbers with sizes e.g. for writing non-structural recursive
functions over them (like integer division), while in effect
writing something else, with unpleasant consequences.</p>
</body>
</html>