
<html>

  <head>


    <meta http-equiv="content-type" content="text/html; charset=utf-8">

  </head>

  <body bgcolor="#FFFFFF" text="#000000">

    The definition of "strictly positive" for data types is given <a

href="https://agda.readthedocs.io/en/latest/language/data-types.html#strict-positivity">here</a>,

    but apparently it's different for record types, ruling out *any*

    occurrence to the left of an arrow (not just those in negative

    positions). I doubt that allowing such occurrences could lead to an

    inconsistency. What's the rationale for being so strict about

    positivity?<br>

    <br>

    --okay<br>

    data D : Set₁ where<br>

      d : D → (Set → D) → D<br>

    <br>

    --fails<br>

    record R : Set₁ where<br>

      inductive<br>

      field<br>

        r : (Set → R) → R<br>

    <br>

    --R is not strictly positive, because it occurs<br>

    --to the left of an arrow<br>

    --in the definition of R.<br>

    <br>

  </body>

</html>