[Agda] level setting problem

[Jesper Cockx]

> 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"?)

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
https://agda.readthedocs.io/en/latest/language/universe-levels.html.

-- Jesper


On Sun, Apr 11, 2021 at 8:56 PM Georgi Lyubenov <godzbanebane at gmail.com>
wrote:

> You use the List for its strucutre/spine effectively only, so it can be
> reduced to a Nat instead at least.
>
> 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:
>
> n = 0:
> makeLevels [] = a , b
> done
>
> n = 1:
> makeLevels (x :: []) =>
> let (c , d) = makeLevels [] in (c ⊔ d , c ⊔ d) =>
> (a ⊔ b , a ⊔ b)
> done
>
> n = n' + 2:
>
> makeLevels (x :: xs) =
> let (c , d) = makeLevels xs in (c ⊔ d , c ⊔ d) => // by ih c = a ⊔ b and d
> = a ⊔ b
> ((a ⊔ b) ⊔ (a ⊔ b) , (a ⊔ b) ⊔ (a ⊔ b))
>
> 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"?)
>
> If they are, then my argument should hold.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210411/2848f46e/attachment.html>