[Agda] Induction from Sigma?

[Jakob von Raumer]

Hi Joey,

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.

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

Cheers

Jakob

On 09/04/2020 07:59, Joey Eremondi wrote:
> 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!
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200409/8145af73/attachment.html>