<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;">My experience, as an occasional user of this stuff, is that `Size<` is

broken, and you have to make do with `↑`, `_⊔_`, &c. This makes it a

really bad thing that the example in the documentation uses `Size<` (if

my impressions are correct).

James

</pre>

        <br class="Apple-interchange-newline">

      </blockquote>

      The Codata implementations in the standard library also use

      Size< quite extensively: they use Thunks, which use Size<. <br>

    </p>

    <p>I don't see any way of dealing with coinductive (record)

      definitions without Size<.  ↑ works for inductive definitions,

      because, e.g.,  one can write</p>

    <p>    data list {A : Set}: { k : Size} →  Set where<br>

                cons : ∀ {k} →  A → list{A} {k} → list{A} {↑ k} <br>

    </p>

    <p>However, for coinductive records, I don't see how to replace the

      Size< in the standard definition (below) by anything else: </p>

    <p>    record stream{A : Set} {k : Size} : Set where <br>

               coinductive<br>

               field<br>

                  head : A<br>

                  tail :  {j : Size< k} → stream{A} {j}</p>

    <p>I've tried a couple of things but got parsing or typechecking

      errors.  Does anybody know a way to define the above without

      Size< ?</p>

    <p>Best regards</p>

    <p>- Vlad<br>

    </p>

  </body>

</html>