[Agda] Induction from Sigma?

[Joey Eremondi]

I have an inductive type that looks something like this:

data Foo : Set where
  A : (Foo , Foo) -> Foo
  B : (Nat -> Foo) -> Foo
  C : Unit -> Foo

I'm trying to show that P holds for Foo, for some specific P : Set -> Set.
I currently have:

  (A B : Set) -> P A -> P B -> P (A , B)
  (A : Set) -> P A -> P (Nat -> A)
  P Unit
and importantly,
  (I : Set) -> (T : I -> Set) -> ( (i : I) -> P (T i) ) -> P (Sigma I T)
i.e. we can compose P for any n-ary sum type.

What I'm wondering is, is there any way I can combine these to get P Foo?

Some notes:
* 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.
* 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.

My ideas:

* 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.
* Maybe sized types can be used to make an explicit fixed-point operator,
so I can have a recursive sum?
* Could Containers, W-types, Descriptions, levitation, etc. be useful here?

Thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200408/6c3add90/attachment.html>