[Agda-dev] The great resurrection of Prop

[Andreas Abel]

Hi Nicolas,

thanks for hosting Jesper!

Wrt. models, I was hoping for some constructive predicative 
realizability model, but maybe this is not possible.

Best,
Andreas

On 23.02.2018 10:32, nicolas tabareau wrote:
> Hi Andreas,
> 
> (* I'm posting again as I was not on agda-dev mailing list the first time *)
> 
> It was very nice working with Jesper this week.
> 
> Regarding your question on impredicativity, there
> are two ways of justifying it in this setting.
> 
> We know by construction that any inhabitant of
> Prop is HProp in the sense of HoTT, so using
> propositional resizing rule of VV, every inahbitant
> of Prop_i can be lower to Prop_0, so only Prop_0
> is needed.
> 
> In this way, it can be seen as a syntactical version
> of VV propositional resizing rule.
> 
> 
> The other way more direct way of justifying it is
> using a classical model because then Prop is
> just "empty + unit".
> 
> Best,
> 
> -- Nicolas
> 
> 
> 
> On Fri, Feb 23, 2018 at 8:50 AM, Andreas Abel <abela at chalmers.se 
> <mailto:abela at chalmers.se>> wrote:
> 
>     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
>         <https://github.com/jespercockx/agda/tree/prop-rezz>
> 
>         and a short demo file of what's possible at:
> 
>         https://gist.github.com/jespercockx/d7e0885f2078e0c0a54de99117226ac4
>         <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 <mailto:Agda-dev at lists.chalmers.se>
>         https://lists.chalmers.se/mailman/listinfo/agda-dev
>         <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 <mailto:andreas.abel at gu.se>
>     http://www.cse.chalmers.se/~abela/ <http://www.cse.chalmers.se/~abela/>
> 
> 
> 
> 
> -- 
> Nicolas Tabareau
> Researcher at Inria
> Gallinette Team, Nantes
> 
> 
> _______________________________________________
> 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/