decidable.agda

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

module decidable where

open import level using (Level)
open import sets.empty using (⊥; ¬_)
open import sets.unit using (⊤; tt)

-- Decidable relations.

data Dec {i} (P : Set i) : Set i where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

True : ∀ {i}{P : Set i} → Dec P → Set
True (yes _) = ⊤
True (no _) = ⊥

witness : ∀ {i}{P : Set i}{d : Dec P} → True d → P
witness {d = yes x} _ = x
witness {d = no _} ()

decide : ∀ {i} {P : Set i} {d : Dec P} → P → True d
decide {d = yes p} = λ _ → tt
decide {d = no f} = f