[Agda] Rewrite rules for both Set and Prop

[Jesper Cockx]

Hi Filippo,

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 (
https://github.com/agda/agda/issues/3328), 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?

-- Jesper

On Thu, Jan 30, 2020 at 12:31 PM Filippo Sestini <
Filippo.Sestini at nottingham.ac.uk> wrote:

> 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.
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200130/214d950d/attachment.html>