[Agda] level setting problem

[mechvel at scico.botik.ru]

Sorry,
I have missed the point that adding (a ⊔ b) two times
gives the same level as adding it one time.

Thank you.

--
SM



On 2021-04-11 21:55, Georgi Lyubenov 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