[Agda] How experimental is Cumulativity?

[Jon Sterling]

Jesper,

Is the cumulativity support based on "material subtyping" (I mean, elements of one universe really being elements of another universe) or is it based on elaboration of coercions?

In the past I advocated this material subtyping, but these days  I have been won over to coercions... mainly due to my suffering as I try to find models of type theory in places where it is no longer feasible to rely on the set-theoretic trickery which makes material cumulativity acceptable in, for instance, presheaf models a la Coquand.

It also seems like the combination of material subtyping and unification may be a bit difficult to negotiate; I am curious how Agda's implementation deals with this, if it needs to.

Best,
Jon


On Sat, Jan 4, 2020, at 9:07 AM, Jesper Cockx wrote:
> Hi Joey,
> 
> The note that it is experimental mainly refers to the fact that there 
> is no proper solver yet for level (in)equalities, so there will be 
> (possibly quite frequent) cases where you have to fill in implicit 
> level arguments that Agda is able to infer without --cumulativity. That 
> being said, it is also a new feature in Agda and it hasn't been tested 
> very extensively yet so there may also still be bugs of the "make Agda 
> unsound" kind. Running Agda with the --double-check flag enabled might 
> catch some of these bugs when they occur.
> 
> -- Jesper
> 
> ps: If anyone is interested in implementing a proper solver for 
> universe levels, please get in touch! There may be some interesting 
> research questions lurking there.
> 
> On Fri, Jan 3, 2020 at 8:28 PM Joey Eremondi <joey.eremondi at gmail.com> wrote:
> > I see that Cumulativity is listed as an experimental feature in 2.6.1. Is this "the compiler might crash or reject valid programs" experimental? Or "Cumulativity might make Agda unsound" experimental? How much can I trust proofs that use cumulative Agda?
> > 
> > Thanks!
> >  _______________________________________________
> >  Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>