[Agda] Moving Prop under Quantifiers?

[Guillaume Brunerie]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200705/6cc79881/attachment.html>