[Agda] Induction from Sigma?

[Thorsten Altenkirch]

Hi Joey,

Sorry but your question doesn’t make much sense to me. Maybe you can tell us what you want to do in more elementary terms.

Btw, I don’t know what “(Foo , Foo)” is supposed to mean. We are not doing Haskell here. I guess you mean Foo x Foo?

You say that you want to show that “P holds for Foo”? What is P? It seems that you are thinking of a property of types. There are some properties of types, like being finite or having at most one element and so on, but not so many. And since all properties of types are closed under isomorphism P must also hold for them. I guess this means you could omit A anyway.

What does it mean that “P holds under isomorphism”?

Sorry,
Thorsten

From: Agda <agda-bounces at lists.chalmers.se> on behalf of Joey Eremondi <joey.eremondi at gmail.com>
Date: Thursday, 9 April 2020 at 06:59
To: Agda mailing list <agda at lists.chalmers.se>
Subject: [Agda] Induction from Sigma?

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!




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200409/e161accd/attachment.html>