<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:x="urn:schemas-microsoft-com:office:excel" 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;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
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="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">You can’t have a cake and eat it. However, if you add enough equalities to identify equivalent ordinals then you may get what you want. This requires thought.<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">Cheers,<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>
<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"><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 Guillaume Brunerie <guillaume.brunerie@gmail.com><br>
<b>Date: </b>Sunday, 5 July 2020 at 21:32<br>
<b>To: </b>Joey Eremondi <joey.eremondi@gmail.com><br>
<b>Cc: </b>Agda mailing list <agda@lists.chalmers.se><br>
<b>Subject: </b>Re: [Agda] Moving Prop under Quantifiers?<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">No, unfortunately you cannot define something in Set by induction over something in Prop (and you wouldn't be able to get out of a Squash either), and I don't know of any good workaround for that. If you really need to define something
in Set by induction on the ordering, you may need to keep your ordering in Set. <o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Best, <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Guillaume <o:p></o:p></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">Den sön 5 juli 2020 21:25Joey Eremondi <<a href="mailto:joey.eremondi@gmail.com" target="_blank">joey.eremondi@gmail.com</a>> skrev:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal">Thanks Nicolai and Guillaume.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">The next question is, if I've defined a datatype in Prop, is it possible to do Well-founded induction on it? That's what I need the orderings for, but I'm not certain that it will be proof irrelevant...<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">On Sat, Jul 4, 2020 at 4:14 PM Joey Eremondi <<a href="mailto:joey.eremondi@gmail.com" target="_blank">joey.eremondi@gmail.com</a>> wrote:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal">I have a type f Brouwer ordinals Ord, where one of the constructors is (lim : (Nat -> Ord) -> Ord). I've got an ordering on ordinals, where one of the constructors is
<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">(lim< : (f : Nat -> Ord) (o : Ord) -> ((a : Nat) -> f a < o) -> lim f < o).<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I'm using the ordinals to bound the size of data structures, but I want the bounds to be irrelevant, so I've been using Squash: Set -> Prop (as defined in the Prop docs) to define an irrelevant version of this. The problem is, when I'm
producing proofs of (Squash (o1 < o2)), I can't figure out a way to use the lim< constructor.
<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Basically, I'm wondering, given the lim constructor above, (squash : A -> Squash a), and squash-elim : (A : Set) (P : Prop) -> (A -> P) -> Squash A -> P, if there's any way to write the following function:<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">p-lim< : (f : Nat -> Ord) (o : Ord) -> ((a : Nat) -> Squash (f a < o)) -> Squash (lim f < o))<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">That is, if I have a function that produces the necessary "squashed" proof for each Nat, is there a way I can move the entire function into Prop. In principle, what I'm doing doesn't go against Prop, i.e. I'm only matching on Prop values
when I'm producing a *final* value in Prop. But the intermediate steps leave Prop, which is what is causing problems.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Is this just a limitation of Prop? Is the old dotted-irrelevance any different? Or is there some way to do this that I'm not seeing?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Thanks!<o:p></o:p></p>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><o:p></o:p></p>
</blockquote>
</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>