<div dir="auto">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. <div dir="auto"><br></div><div dir="auto">Best, </div><div dir="auto">Guillaume </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Den sön 5 juli 2020 21:25Joey Eremondi <<a href="mailto:joey.eremondi@gmail.com" target="_blank" rel="noreferrer">joey.eremondi@gmail.com</a>> skrev:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>Thanks Nicolai and Guillaume.</div><div><br></div><div>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...</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Jul 4, 2020 at 4:14 PM Joey Eremondi <<a href="mailto:joey.eremondi@gmail.com" rel="noreferrer noreferrer" target="_blank">joey.eremondi@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>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 <br></div><div>(lim< : (f : Nat -> Ord) (o : Ord) -> ((a : Nat) -> f a < o) -> lim f < o).</div><div><br></div><div>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. <br></div><div><br></div><div>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:</div><div>p-lim< : (f : Nat -> Ord) (o : Ord) -> ((a : Nat) -> Squash (f a < o)) -> Squash (lim f < o))</div><div><br></div><div>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.</div><div><br></div><div>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?</div><div><br></div><div>Thanks!<br></div></div>
</blockquote></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" rel="noreferrer noreferrer" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>