[Agda] Moving Prop under Quantifiers?

[Nicolai Kraus]

Hi Joey,
it sounds like you want to do something that requires countable choice. 
See the HoTT book, Chapter 11.3 for a discussion on this 
(https://homotopytypetheory.org/book/).
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 :-)
Nicolai

On 05/07/2020 00:14, Joey Eremondi wrote:
> 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!
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200705/7658feb8/attachment.html>