------------------------------------------------------------------------
-- The Agda standard library
--
-- Negation indexed by a Level
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Relation.Nullary.Indexed where

open import Data.Empty hiding (⊥-elim)
open import Level

------------------------------------------------------------------------
-- Negation.

-- level polymorphic version of ¬
¬ :  {} (b : Level)  Set   Set (  b)
¬ b P = P  Lift b