<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>