[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