[Agda] Issue with sized types (max of two sizes less than i)

[Nils Anders Danielsson]

On 2018-09-27 18:45, Guillaume Brunerie wrote:
> It seems related to the following question: given j and k of type
> Size< i, is j ⊔ˢ k also of type Size< i?

I tried giving the arguments explicitly:

   f {i} (cons {j₁} x l1) (cons {j₂} _ l2) =
     cons {i} {j₁ ⊔ˢ j₂} x (f {j₁ ⊔ˢ j₂} l1 l2)

Agda still complained. I suggest that you report this as a bug.

-- 
/NAD