[Agda] Rewrite rules for both Set and Prop

[Filippo Sestini]

Hi all,

I'm trying to encode an equality type in Agda using rewrite rules.
I want the type to be a strict proposition, so I value it in the Prop universe.
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).

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.

Am I missing something here? Does anybody know a way out of this?

Thank you
-- 
Filippo Sestini
 




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.