<div dir="ltr"><div>Hi Jon,</div><div><br></div><div>It's using material subtyping, so there's no coercions involved in the resulting terms. You make a good point about the difficulty of finding models, but I felt inserting actual coercions would be too hard to work with in practical programming (essentially not much better than using Lift in non-cumulative Agda). Perhaps a different approach where the coercion from Set_i to Set_{i+k} commutes with other type formers would be another viable solution if the current approach doesn't work.</div><div><br></div><div>You're correct that the interaction between material subtyping and unification is quite tricky, currently Agda applies a few heuristics to simplify equations between universe levels. If you are interested, you can take a look at the functions `equalLevel` and `leqLevel` in Conversion.hs (<a href="https://github.com/agda/agda/blob/dcb0f82f90fe44114d43303524a6fab5051bdaa2/src/full/Agda/TypeChecking/Conversion.hs#L1384">https://github.com/agda/agda/blob/dcb0f82f90fe44114d43303524a6fab5051bdaa2/src/full/Agda/TypeChecking/Conversion.hs#L1384</a> and <a href="https://github.com/agda/agda/blob/dcb0f82f90fe44114d43303524a6fab5051bdaa2/src/full/Agda/TypeChecking/Conversion.hs#L1244">https://github.com/agda/agda/blob/dcb0f82f90fe44114d43303524a6fab5051bdaa2/src/full/Agda/TypeChecking/Conversion.hs#L1244</a>) and `simplifyLevelConstraint` in LevelConstraints.hs (<a href="https://github.com/agda/agda/blob/dcb0f82f90fe44114d43303524a6fab5051bdaa2/src/full/Agda/TypeChecking/LevelConstraints.hs#L25">https://github.com/agda/agda/blob/dcb0f82f90fe44114d43303524a6fab5051bdaa2/src/full/Agda/TypeChecking/LevelConstraints.hs#L25</a>). Really what we need is a good solver for level constraints. I think the problem is quite similar to the analogous one for sized types (which also is implemented using material subtyping), so my hope is that one solver could be general enough to handle both subsystems.</div><div><br></div><div>-- Jesper<br></div><div><br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Jan 4, 2020 at 3:35 PM Jon Sterling <<a href="mailto:jon@jonmsterling.com" target="_blank">jon@jonmsterling.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Jesper,<br>
<br>
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?<br>
<br>
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.<br>
<br>
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.<br>
<br>
Best,<br>
Jon<br>
<br>
<br>
On Sat, Jan 4, 2020, at 9:07 AM, Jesper Cockx wrote:<br>
> Hi Joey,<br>
> <br>
> The note that it is experimental mainly refers to the fact that there <br>
> is no proper solver yet for level (in)equalities, so there will be <br>
> (possibly quite frequent) cases where you have to fill in implicit <br>
> level arguments that Agda is able to infer without --cumulativity. That <br>
> being said, it is also a new feature in Agda and it hasn't been tested <br>
> very extensively yet so there may also still be bugs of the "make Agda <br>
> unsound" kind. Running Agda with the --double-check flag enabled might <br>
> catch some of these bugs when they occur.<br>
> <br>
> -- Jesper<br>
> <br>
> ps: If anyone is interested in implementing a proper solver for <br>
> universe levels, please get in touch! There may be some interesting <br>
> research questions lurking there.<br>
> <br>
> On Fri, Jan 3, 2020 at 8:28 PM Joey Eremondi <<a href="mailto:joey.eremondi@gmail.com" target="_blank">joey.eremondi@gmail.com</a>> wrote:<br>
> > 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?<br>
> > <br>
> > Thanks!<br>
> >  _______________________________________________<br>
> >  Agda mailing list<br>
> > <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>