[Agda-dev] The great resurrection of Prop

[nicolas tabareau]

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



-- 
Nicolas Tabareau
Researcher at Inria
Gallinette Team, Nantes
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20180223/d9d92032/attachment.html>