[Agda-dev] The great resurrection of Prop

[Jesper Cockx]

Hi Agda developers,

This week I was visiting the Coq people in Nantes who are working on adding
a new sort sProp of definitionally proof irrelevant propositions to Coq.
Just for fun, I tried to see how easy it would be to add something similar
to Agda. As it turns out, there was still some (unused) legacy code for
Prop laying about, and making it do something sensible was surprisingly
straightforward. I'm sure the result is still a buggy mess, but if you want
to try it out, you can find the code at:

https://github.com/jespercockx/agda/tree/prop-rezz

and a short demo file of what's possible at:

https://gist.github.com/jespercockx/d7e0885f2078e0c0a54de99117226ac4

One known issue is that sometimes Agda chooses to instantiate a sort to
Prop too eagerly, so you may have to be more explicit than usual in giving
the types of arguments. In particular, you have to write `{a : Level}`
rather than `∀ {a}` when writing universe-polymorphic code. The reason for
this is that Agda still doesn't have proper sort metas, but this is a
problem not limited to Prop (I remember it also being a problem for sized
types and for my failed attempt at implementing --omega-in-omega at the
Agda meeting).

Once this issue is solved, we could consider having Prop in Agda instead of
(or in addition to) the current irrelevant function spaces. In particular,
this would allow us to have irrelevant return types and to quantify over
all irrelevant types. Let me know what you think!

Cheers,
Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20180222/289cf3d0/attachment.html>