[Agda-dev] The great resurrection of Prop

[Andreas Abel]

Hi Jesper,

thanks for the heads up from Nantes!  I'd be excited by such an extension!

 > 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)

Indeed, the sort handling would need a makeover, to properly host sorts 
beyond the linear order of Set_i.  Also sort metas are needed, and 
conversion checking could be blocked on a sort meta.

 > 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!

It makes perfectly sense to me to have a universe Prop of squashed types 
in addition to squashing types in function type domains.
However, wouldn't we need a hierarchy of Prop universes?

Cheers,
Andreas

On 22.02.2018 20:26, Jesper Cockx wrote:
> 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
> 
> 
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
> 

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/