module negation where

open import level
open import empty

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infix 7 ¬_

----------------------------------------------------------------------
-- defined types
----------------------------------------------------------------------

¬_ : ∀{ℓ}(x : Set ℓ) → Set ℓ
¬ x = x → ⊥