why do i feel guilty about import Agda.Primitive renaming (Set to Type)
Conversation
It's the way of the future!
1
why is monad like this
1
what is wrong?
2
this is my library, it complains about an unsolved level
record Monad {a b} (M : Set a → Set b) : Set (lsuc (a ⊔ b)) where
1