Vojtěch Štěpančík
Vojtěch Štěpančík
That sounds reasonable to me
I would read it as relating to `UU omega`, but it's true that we already have a naming convention for that sort of types, and that's `Large-`
I think this needs some documentation on how eta equality is used in the library and what are the consequences. One non-obvious consequence of this change is that if you...
See also how a similar situation was handled in cubical https://github.com/agda/cubical/pull/1021 and the discussion linked there. IIUC the final resolution was for the 1lab (where the code was adapted from,...