Agda: Which part does this type introduce universe inconsistency?
The term you're applying ¬_ to is large: it quantifies over all M : Set and therefore has type Set 1. So instead of ¬_ : Set -&gt; Set you need ¬_ : Set 1 -&gt; Set 1.

A more general solution it to make ¬_ level polymorphic as in the standard library: you will be able to use this definition of negation across the board no matter how large the thing you're negating is.