<div dir="ltr"><div>Hi Filippo,</div><div><br></div><div>You're correct that you currently cannot do this, as there's no way to define types that are polymorphic over both Set and Prop (<a href="https://github.com/agda/agda/issues/3328">https://github.com/agda/agda/issues/3328</a>), and you can only have one rewriting relation. However, I don't understand why you would want rewrite rules to rewrite elements of a Prop, since they are anyway all equal?</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 30, 2020 at 12:31 PM Filippo Sestini <<a href="mailto:Filippo.Sestini@nottingham.ac.uk">Filippo.Sestini@nottingham.ac.uk</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">Hi all,<br>
<br>
I'm trying to encode an equality type in Agda using rewrite rules.<br>
I want the type to be a strict proposition, so I value it in the Prop universe.<br>
However, this also means that among the equations that I want to encode as rewrite rules, some will end up being between elements of a Set (for example, when rewriting the eq type itself) and some will be between elements of a Prop (for example, the elements of the identity type itself).<br>
<br>
I'm struggling to find a way to do this with Agda's rewriting system. As far as I know there is no way to define an identity type that works for both types in Set and in Prop. One could define two different identity types for each, but unfortunately Agda doesn't seem to allow declaring two different relations for BUILTIN REWRITE.<br>
<br>
Am I missing something here? Does anybody know a way out of this?<br>
<br>
Thank you<br>
-- <br>
Filippo Sestini<br>
<br>
<br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please contact the sender and delete the email and<br>
attachment. <br>
<br>
Any views or opinions expressed by the author of this email do not<br>
necessarily reflect the views of the University of Nottingham. Email<br>
communications with the University of Nottingham may be monitored <br>
where permitted by law.<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>