# 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.
• yeah, after I took a shower I realized that too. i think -> is also a type constructor, the universe of which is the larger one of the ones of both operands. is that understanding correct? – Jason Hu Feb 14 '18 at 18:55