{-# OPTIONS --cubical-compatible #-}
module Terra.Data.Negation where
open import Terra.Data.Level
open import Terra.Data.Counit

private
  variable
    ℓ : Level

¬_ : Set ℓ -> Set ℓ
¬_ P = (f : P) -> ⊥


infix  ¬_