<div dir="ltr"><div dir="ltr">> This is the only part I'm not sure about - is ⊔ commutative and associative, and is x ⊔ x == x? (And of course, does agda solve these equations "under the hood"?)</div><div dir="ltr"><br></div><div>The answers are yes and yes and yes. Agda has a special internal representation of levels which takes into account commutativity, associativity, and idempotence, as well as neutrality of lzero (`lzero ⊔ x == x`), subsumption (e.g. `x ⊔ lsuc x == lsuc x`), and distributivity of lsuc over ⊔ (`lsuc (x ⊔ y) == lsuc x ⊔ lsuc y`). It would actually nice to have something about this documented in the user manual at <a href="https://agda.readthedocs.io/en/latest/language/universe-levels.html">https://agda.readthedocs.io/en/latest/language/universe-levels.html</a>.</div><div><br></div><div>-- Jesper<br></div><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Apr 11, 2021 at 8:56 PM Georgi Lyubenov <<a href="mailto:godzbanebane@gmail.com">godzbanebane@gmail.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"><div dir="ltr">You use the List for its strucutre/spine effectively only, so it can be reduced to a Nat instead at least.<br><br>Upon a further look, as far as I can tell, your function makeLevels returns (a , b) if the list is empty, and (a ⊔ b , a ⊔ b) otherwise:<br><br>n = 0:<br>makeLevels [] = a , b<br>done<br><br>n = 1:<br>makeLevels (x :: []) =><br>let (c , d) = makeLevels [] in (c ⊔ d , c ⊔ d) =><br>(a ⊔ b , a ⊔ b)<br>done<br><br>n = n' + 2:<br><br>makeLevels (x :: xs) = <br>let (c , d) = makeLevels xs in (c ⊔ d , c ⊔ d) => // by ih c = a ⊔ b and d = a ⊔ b<br>((a ⊔ b) ⊔ (a ⊔ b) , (a ⊔ b) ⊔ (a ⊔ b)) <br><br>This is the only part I'm not sure about - is ⊔ commutative and associative, and is x ⊔ x == x? (And of course, does agda solve these equations "under the hood"?)<br><br>If they are, then my argument should hold.</div>
_______________________________________________<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></div>