[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Andreas Abel]

On 05.01.2017 20:19, Roman wrote:
> Andreas, does it mean that the whole forcing business is hazardous? As
> "the lowest level equality" is just an instance of it.

Can you give an example please?


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/