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