[Agda] Moving Prop under Quantifiers?

[Joey Eremondi]

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
(lim< : (f : Nat -> Ord) (o : Ord) -> ((a : Nat) -> f a < o) -> lim f < o).

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.

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:
p-lim< : (f : Nat -> Ord) (o : Ord) -> ((a : Nat) -> Squash (f a < o)) ->
Squash (lim f < o))

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.

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?

Thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200704/b551de1f/attachment.html>