[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Roman]

Andreas, does it mean that the whole forcing business is hazardous? As
"the lowest level equality" is just an instance of it.