<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></div><div><br></div></div>