module examplenegbool where

data Bool : Set where
  tt : Bool
  ff : Bool


data ⊤ : Set where
  true : ⊤ 


data ⊥ : Set where


¬Bool : Bool -> Bool  
¬Bool tt = ff
¬Bool ff = tt