[Agda] level setting problem

[Georgi Lyubenov]

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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210411/aa892331/attachment.html>