Bálint Kocsis

icon indicating an email [email protected]

icon location PhD student at Radboud University. Currently working on categorical automata theory.

Results 1 comments of Bálint Kocsis

total Omega : ⊥

In Agda, this piece of code is rejected because the universe of the type of the constructor `Abs` is `Set_1`, which is higher than `Set_0`, the universe of the data...