Agda: Which part does this type introduce universe inconsistency?

I was trying to prove following lemma,

my_thm : ¬ (∀ {M : Set} (P Q : M → M → Set) →
    (∀ x → ∃ M , λ y → P x y ∨ Q x y) →
    (∀ x → ∃ M , P x) ∨ (∀ x → ∃ M , Q x))
  my_thm = ?

while Agda gives following mistake:

Set₁ != Set
when checking that the expression
{M : Set} (P Q : M → M → Set) →
(∀ x → ∃ M , λ y → P x y ∨ Q x y) →
(∀ x → ∃ M , P x) ∨ (∀ x → ∃ M , Q x)
has type Set

honestly, in my untrained eyes, this type looks entirely routine to me, and it shouldn't introduce universe inconsistency.

all extra quantifier and connectivities are defined as following,

data _∨_ : Set → Set → Set where
    inl : {A B : Set} → A → A ∨ B
    inr : {A B : Set} → B → A ∨ B
  infixl 20 _∨_

  ¬_ : Set → Set
  ¬ P = P → False
  infix 40 ¬_

  data ∃_,_ : (A : Set) → (A → Set) → Set where
    ex : {A : Set}{P : A → Set} → (x : A) → (ev : P x) → ∃ A , P
  infix 10 ∃_,_

which part introduces Set1 in this code?

ok, it turns out it's caused by negation: ¬_ : Set → Set. However, I still not understand. why this innocent looking function does not do what I want? what's the correct way of implementing it?

The term you're applying ¬_ to is large: it quantifies over all M : Set and therefore has type Set 1. So instead of ¬_ : Set -> Set you need ¬_ : Set 1 -> 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.

StackExchange Computer Science Q#88077, answer score: 6