[Agda] Moving Prop under Quantifiers?

[Thorsten Altenkirch]

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.

Cheers,
Thorsten


From: Agda <agda-bounces at lists.chalmers.se> on behalf of Guillaume Brunerie <guillaume.brunerie at gmail.com>
Date: Sunday, 5 July 2020 at 21:32
To: Joey Eremondi <joey.eremondi at gmail.com>
Cc: Agda mailing list <agda at lists.chalmers.se>
Subject: Re: [Agda] Moving Prop under Quantifiers?

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.

Best,
Guillaume

Den sön 5 juli 2020 21:25Joey Eremondi <joey.eremondi at gmail.com<mailto:joey.eremondi at gmail.com>> skrev:
Thanks Nicolai and Guillaume.

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


On Sat, Jul 4, 2020 at 4:14 PM Joey Eremondi <joey.eremondi at gmail.com<mailto:joey.eremondi at gmail.com>> 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<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda



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.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200706/5875f7d4/attachment.html>