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