<div dir="ltr"><div dir="ltr"><div>Hi Simon,</div><div><br></div><div>It would be easy to add such a flag, but unfortunately it would also be unsound since Agda's termination checker currently assumes predicativity:</div><div><br></div><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">data ⊥ : Prop where<br><br>data Weird : Prop where<br>  weird : (∀ {A : Prop} → A → A) → Weird<br><br>yes : Weird<br>yes = weird (λ x → x)<br><br>no : Weird → ⊥<br>no (weird f) = no (f (weird f))<br><br>boom : ⊥<br>boom = no yes<br></blockquote></div><div><br></div><div>Changing the termination checker to remove this assumption would take some more work. Would you be happy with a version of --impredicative-prop which is essentially a limited version of --type-in-type (and is thus unsound)?</div><div><br></div><div>-- Jesper<br></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Wed, Oct 10, 2018 at 10:20 AM Simon Boulier <<a href="mailto:simon.boulier@ens-rennes.fr">simon.boulier@ens-rennes.fr</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi all,<br>
<br>
I need an impredicative Prop universe.<br>
<br>
Would it be lot of work to add an experimental "--impredicative-prop" flag?<br>
<br>
I am also aware of this hack of Martin Escardo:<br>
<a href="http://www.cs.bham.ac.uk/~mhe/impredicativity/" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe/impredicativity/</a><br>
But I am not sure to which extent I can adapt it to my needs...<br>
<br>
Cheers,<br>
<br>
<br>
Simon<br>
<br>
<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>