[Agda] Defining equality in Prop

[Bob Atkey]

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