module test where
open import Data.Empty
open import Relation.Binary.PropositionalEquality

data Not (A : Set) : Set where not : .(A → ⊥) → Not A

irr-bot : .⊥ → ⊥
irr-bot ()

not-elim : ∀{A} → Not A → (A → ⊥)
not-elim (not y) a = irr-bot (y a)

neg-not : ∀{A} → (A → ⊥) → Not A
neg-not = not

not-uniq : ∀{A} → (p1 p2 : Not A) → p1 ≡ p2
not-uniq (not _) (not _) = refl