module Logic where infix 60 ¬_ data ⊥ : Set where record ⊤ : Set where constructor tt ¬_ : Set → Set ¬ A = A → ⊥