[Agda] Moving Prop under Quantifiers?

[Joey Eremondi]

Fair enough. My hope was that if the thing in Prop was irrelevant to the
actual result, and only served as a witness to the termination, that it
would work. I'll just try moving it to Set and manually proving that things
are equal. Thanks!

On Mon, Jul 6, 2020 at 4:05 AM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> 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> 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>
> 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
>
> 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/7e80017b/attachment.html>