4
$\begingroup$

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?

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Jason Hu Feb 14 '18 at 18:55
  • 1
    $\begingroup$ You're correct. $\endgroup$ – gallais Feb 14 '18 at 19:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.