[Agda] Defining equality in Prop

[András Kovács]

Hi,

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:
https://dl.acm.org/doi/pdf/10.1145/3290316

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.

Bob Atkey <bob.atkey at gmail.com> ezt írta (időpont: 2020. jún. 23., K,
16:55):

> Hello,
>
> I've been experimenting with using the rewrite rules in Agda to
> implement a simple axiomatisation of parametricity that I've proved
> sound in the reflexive graph model. Here is my current development:
>
> https://gist.github.com/bobatkey/7861009f7d28d568eec8f8c32dd07b28
>
> For the soundness of the axiomatisation, it is important that the
> relational interpretations of small types are proof irrelevant. I am
> using the Prop sort to do this.
>
> However, the most common relations are variants on equality. One can
> define an equality type in Prop, however, as the documentation for Prop
> points out, this is nearly useless because one cannot eliminate the
> equality into Set to prove subst, transport, etc.
>
> Coming from Coq, I would have thought that eliminating a single
> constructor data type like equality into Set ought to be safe, even if
> it is defined in Prop. Is there some deep reason why this is not
> possible in Agda, or is it just that it has not been implemented?
>
> Thanks,
>
> Bob
>
> _______________________________________________
> 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/20200623/65f06ae7/attachment.html>