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