<div dir="ltr">Fair enough. My hope was that if the thing in Prop was irrelevant to the actual result, and only served as a witness to the termination, that it would work. I'll just try moving it to Set and manually proving that things are equal. Thanks!<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Jul 6, 2020 at 4:05 AM Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">





<div lang="EN-GB">
<div class="gmail-m_-3179402813435682709WordSection1">
<p class="MsoNormal"><span>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.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Cheers,<u></u><u></u></span></p>
<p class="MsoNormal"><span>Thorsten<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div style="border-color:rgb(181,196,223) currentcolor currentcolor;border-style:solid none none;border-width:1pt medium medium;padding:3pt 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:12pt;color:black">From: </span></b><span style="font-size:12pt;color:black">Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Guillaume Brunerie <<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>><br>
<b>Date: </b>Sunday, 5 July 2020 at 21:32<br>
<b>To: </b>Joey Eremondi <<a href="mailto:joey.eremondi@gmail.com" target="_blank">joey.eremondi@gmail.com</a>><br>
<b>Cc: </b>Agda mailing list <<a href="mailto:agda@lists.chalmers.se" target="_blank">agda@lists.chalmers.se</a>><br>
<b>Subject: </b>Re: [Agda] Moving Prop under Quantifiers?<u></u><u></u></span></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></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. <u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Best, <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Guillaume <u></u><u></u></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></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:<u></u><u></u></p>
</div>
<blockquote style="border-color:currentcolor currentcolor currentcolor rgb(204,204,204);border-style:none none none solid;border-width:medium medium medium 1pt;padding:0cm 0cm 0cm 6pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<p class="MsoNormal">Thanks Nicolai and Guillaume.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></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...<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></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:<u></u><u></u></p>
</div>
<blockquote style="border-color:currentcolor currentcolor currentcolor rgb(204,204,204);border-style:none none none solid;border-width:medium medium medium 1pt;padding:0cm 0cm 0cm 6pt;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
<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">(lim< : (f : Nat -> Ord) (o : Ord) -> ((a : Nat) -> f a < o) -> lim f < o).<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></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.
<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></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:<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">p-lim< : (f : Nat -> Ord) (o : Ord) -> ((a : Nat) -> Squash (f a < o)) -> Squash (lim f < o))<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></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?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">Thanks!<u></u><u></u></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><u></u><u></u></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></div>

</blockquote></div>