-- Some proposition constructors.

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

module Tools.Nullary where

open import Tools.Empty

-- Negation.

infix 3 ¬_

¬_ : Set  Set
¬ P = P  

-- Decidable propositions.

data Dec (P : Set) : Set where
  yes : ( p :   P)  Dec P
  no  : (¬p : ¬ P)  Dec P

-- If A and B are logically equivalent, then so are Dec A and Dec B.

map :  {A B}  (A  B)  (B  A)  Dec A  Dec B
map f g (yes p) = yes (f p)
map f g (no ¬p) = no  x  ¬p (g x))