<div dir="ltr">Hi,<div><br></div><div>The Prop in Agda is meant to be compatible with univalence. An identity type in Prop which eliminates into Set is not compatible with that. For this and other reasons, the conditions for eliminating into Set are more complicated than just having a single constructor. See the paper: <a href="https://dl.acm.org/doi/pdf/10.1145/3290316">https://dl.acm.org/doi/pdf/10.1145/3290316</a> </div><div><br></div><div>You can still postulate the identity type which you want, and use rewrite rules to define elimination. I believe that this is consistent, because such an identity type is justified e.g. by the setoid model. I've personally used this identity type a few times.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Bob Atkey <<a href="mailto:bob.atkey@gmail.com">bob.atkey@gmail.com</a>> ezt írta (időpont: 2020. jún. 23., K, 16:55):<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hello,<br>
<br>
I've been experimenting with using the rewrite rules in Agda to <br>
implement a simple axiomatisation of parametricity that I've proved <br>
sound in the reflexive graph model. Here is my current development:<br>
<br>
<a href="https://gist.github.com/bobatkey/7861009f7d28d568eec8f8c32dd07b28" rel="noreferrer" target="_blank">https://gist.github.com/bobatkey/7861009f7d28d568eec8f8c32dd07b28</a><br>
<br>
For the soundness of the axiomatisation, it is important that the <br>
relational interpretations of small types are proof irrelevant. I am <br>
using the Prop sort to do this.<br>
<br>
However, the most common relations are variants on equality. One can <br>
define an equality type in Prop, however, as the documentation for Prop <br>
points out, this is nearly useless because one cannot eliminate the <br>
equality into Set to prove subst, transport, etc.<br>
<br>
Coming from Coq, I would have thought that eliminating a single <br>
constructor data type like equality into Set ought to be safe, even if <br>
it is defined in Prop. Is there some deep reason why this is not <br>
possible in Agda, or is it just that it has not been implemented?<br>
<br>
Thanks,<br>
<br>
Bob<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>