On 2020-10-03 15:24, James Wood wrote: > My experience, as an occasional user of this stuff, is that `Size<` is > broken, and you have to make do with `↑`, `_⊔_`, &c. The problems are not restricted to Size<_: https://github.com/agda/agda/issues/2820#issuecomment-704172549 -- /NAD