module My.SetTheory.Relation.Decidable where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Data.Sum as DS
import Level as L
import Relation.Nullary as RN

open DS using (_⊎_)

-- §──────────────────────────────────────────────────────────────────
-- A proposition A is decidable iff either A or not A holds.
-- §──────────────────────────────────────────────────────────────────

decA⇒A⊎¬A : {𝓁 : L.Level} → {A : Set 𝓁} → RN.Dec A → A ⊎ RN.¬ A
decA⇒A⊎¬A (RN.yes a) = DS.inj₁ a
decA⇒A⊎¬A (RN.no ¬a) = DS.inj₂ ¬a

A⊎¬A⇒decA : {𝓁 : L.Level} → {A : Set 𝓁} → A ⊎ RN.¬ A → RN.Dec A
A⊎¬A⇒decA (DS.inj₁ a) = RN.yes a
A⊎¬A⇒decA (DS.inj₂ ¬a) = RN.no ¬a