[Agda] [newbie] universe levels and BUILTIN EQUALITY

Roman effectfully at gmail.com
Thu Jan 5 20:19:31 CET 2017


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


More information about the Agda mailing list