[Agda] Defining equality in Prop

[Andrew M. Pitts]

> On 23 Jun 2020, at 15:53, Bob Atkey <bob.atkey at gmail.com> wrote:
> 
> 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?

I have found the proof irrelevant Prop in recent versions of Agda to be very useful indeed in the context of type theory with uniqueness of identity proofs (Axiom K) and heterogeneous Prop-valued equality, so long as one postulates the Axiom of Unique Choice (A!C), enabling one to soundly escape from Prop to Set, if you see what I mean. The attached example file contains a formulation of A!C and the definite descriptions it enables, towards the end.

Andy

-------------- next part --------------
A non-text attachment was scrubbed...
Name: PropLogic.agda
Type: application/octet-stream
Size: 4206 bytes
Desc: PropLogic.agda
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200623/1e9a360d/attachment.obj>