module Decide where open import Logic data Dec P : Set where no : (np : ¬ P) → Dec P yes : (p : P) → Dec P open import Bool unbool : (x : Bool) → Dec (IsTrue x) unbool true = yes tt unbool false = no (λ x → x)