<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
Hi Joey,<br>
it sounds like you want to do something that requires countable
choice. See the HoTT book, Chapter 11.3 for a discussion on this (<a
href="https://homotopytypetheory.org/book/">https://homotopytypetheory.org/book/</a>).<br>
The HoTT-style solution to this problem is to squash (_<_)
already in its definition, not afterwords. I know that this works
with hProp (a type that you can define yourself), I don't know
whether current Agda can do this with Prop, but I won't be surprised
if it can :-)<br>
Nicolai<br>
<br>
<div class="moz-cite-prefix">On 05/07/2020 00:14, Joey Eremondi
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CADT+LxoHMrvRiry1DQtK81ptMvXk7-Kuov9ErLoezWmGdn1L_Q@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div>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 <br>
</div>
<div>(lim< : (f : Nat -> Ord) (o : Ord) -> ((a : Nat)
-> f a < o) -> lim f < o).</div>
<div><br>
</div>
<div>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. <br>
</div>
<div><br>
</div>
<div>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:</div>
<div>p-lim< : (f : Nat -> Ord) (o : Ord) -> ((a : Nat)
-> Squash (f a < o)) -> Squash (lim f < o))</div>
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>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?</div>
<div><br>
</div>
<div>Thanks!<br>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>