<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>Hi Joey,</p>
    <p>I think I understand your question. The answer is that the
      properties that you have for P so far are not sufficient to prove
      P Foo. To see why this is true, consider a version of Foo with the
      first constructor removed. The resulting type is the type of
      infinitely branching trees. You cannot express the type of trees
      by the means of products, functions out of Nat, and sigma types
      only.</p>
    <p>One solution could be to require P to be stable under the
      formation of W-types (i.e. show that (A : Set)(B : A -> Set)
      -> P A -> ((a : A) -> P (B a)) -> P (W A B)) and then
      equivalently express Foo as a W-type (i.e. prove that Foo ≈ W A B
      for some A and B).</p>
    <p>Cheers</p>
    <p>Jakob<br>
    </p>
    <div class="moz-cite-prefix">On 09/04/2020 07:59, Joey Eremondi
      wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CADT+Lxq4LPp3WM3v0-afnpJw8ZbXB9Wi0Gzk+990c6w5Adkdzg@mail.gmail.com">
      <meta http-equiv="content-type" content="text/html; charset=UTF-8">
      <div dir="ltr">
        <div>I have an inductive type that looks something like this:</div>
        <div><br>
        </div>
        <div>data Foo : Set where <br>
        </div>
        <div>  A : (Foo , Foo) -> Foo</div>
        <div>  B : (Nat -> Foo) -> Foo</div>
        <div>  C : Unit -> Foo</div>
        <div><br>
        </div>
        <div>I'm trying to show that P holds for Foo, for some specific
          P : Set -> Set. I currently have:</div>
        <div><br>
        </div>
        <div>  (A B : Set) -> P A -> P B -> P (A , B)</div>
        <div>  (A : Set) -> P A -> P (Nat -> A) <br>
        </div>
        <div>  P Unit</div>
        <div>and importantly,</div>
        <div>  (I : Set) -> (T : I -> Set) -> ( (i : I) -> P
          (T i) ) -> P (Sigma I T)</div>
        <div>i.e. we can compose P for any n-ary sum type.<br>
        </div>
        <div><br>
        </div>
        <div>What I'm wondering is, is there any way I can combine these
          to get P Foo?</div>
        <div><br>
        </div>
        <div>Some notes:</div>
        <div>* I don't want to prove P Foo directly, because I want the
          ability to add constructors and easily compose the proofs into
          a proof of Foo P.<br>
        </div>
        <div>* I'm open to other representations of Foo. The only reason
          I'm not having it as a Sigma type is that that doesn't allow
          for self-reference.</div>
        <div><br>
        </div>
        <div>My ideas:</div>
        <div><br>
        </div>
        <div>* If I can show that P holds under isomorphism, then I can
          show that Foo is isomorphic to (Foo \times Foo) + (Nat ->
          Foo) + Unit. But I'm not certain that this will still be
          well-founded recursion.</div>
        <div>* Maybe sized types can be used to make an explicit
          fixed-point operator, so I can have a recursive sum?</div>
        <div>* Could Containers, W-types, Descriptions, levitation, etc.
          be useful here?</div>
        <div><br>
        </div>
        <div>Thanks!<br>
        </div>
        <div><br>
        </div>
      </div>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
  </body>
</html>