<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-GB" link="#0563C1" vlink="#954F72">
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Hi Joey,<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">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.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">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?<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">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.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">What does it mean that “P holds under isomorphism”?
<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Sorry,<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Thorsten<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="margin-left:36.0pt"><b><span style="font-size:12.0pt;color:black">From:
</span></b><span style="font-size:12.0pt;color:black">Agda <agda-bounces@lists.chalmers.se> on behalf of Joey Eremondi <joey.eremondi@gmail.com><br>
<b>Date: </b>Thursday, 9 April 2020 at 06:59<br>
<b>To: </b>Agda mailing list <agda@lists.chalmers.se><br>
<b>Subject: </b>[Agda] Induction from Sigma?<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">I have an inductive type that looks something like this:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">data Foo : Set where <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> A : (Foo , Foo) -> Foo<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> B : (Nat -> Foo) -> Foo<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> C : Unit -> Foo<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">I'm trying to show that P holds for Foo, for some specific P : Set -> Set. I currently have:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> (A B : Set) -> P A -> P B -> P (A , B)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> (A : Set) -> P A -> P (Nat -> A)
<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> P Unit<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">and importantly,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> (I : Set) -> (T : I -> Set) -> ( (i : I) -> P (T i) ) -> P (Sigma I T)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">i.e. we can compose P for any n-ary sum type.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">What I'm wondering is, is there any way I can combine these to get P Foo?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Some notes:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">* 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.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">* 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.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">My ideas:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">* 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.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">* Maybe sized types can be used to make an explicit fixed-point operator, so I can have a recursive sum?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">* Could Containers, W-types, Descriptions, levitation, etc. be useful here?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Thanks!<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
</div>
</div>
<PRE>
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.
</PRE></body>
</html>