fixes agda#2059 on the model of agda#2336

Author: jamesmckinna

src/Data/List/Relation/Unary/First/Properties.agda

@@ -13,11 +13,12 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any as Any using (here; there)
 open import Data.List.Relation.Unary.First
-import Data.Sum as Sum
-open import Function.Base using (_∘′_; _$_; _∘_; id)
+import Data.Sum.Base as Sum
+open import Function.Base using (_∘′_; _∘_; id)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_)
+import Relation.Nullary.Decidable.Core as Dec
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable)
-open import Relation.Nullary.Negation using (contradiction)
 
 ------------------------------------------------------------------------
 -- map
@@ -80,14 +81,14 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 module _ {a p} {A : Set a} {P : Pred A p} where
 
   first? : Decidable P → Decidable (First P (∁ P))
-  first? P? xs = Sum.toDec
-               $ Sum.map₂ (All⇒¬First contradiction)
-               $ first (Sum.fromDec ∘ P?) xs
+  first? P? = Dec.fromSum
+            ∘ Sum.map₂ (All⇒¬First contradiction)
+            ∘ first (Dec.toSum ∘ P?)
 
   cofirst? : Decidable P → Decidable (First (∁ P) P)
-  cofirst? P? xs = Sum.toDec
-                 $ Sum.map₂ (All⇒¬First id)
-                 $ first (Sum.swap ∘ Sum.fromDec ∘ P?) xs
+  cofirst? P? = Dec.fromSum
+              ∘ Sum.map₂ (All⇒¬First id)
+              ∘ first (Sum.swap ∘ Dec.toSum ∘ P?)
 
 ------------------------------------------------------------------------
 -- Conversion to Any

src/Data/Sum.agda

@@ -15,8 +15,7 @@ open import Data.Unit.Polymorphic.Base using (⊤; tt)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Function.Base
 open import Level
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (Dec; yes; no; _because_; ¬_)
+import Relation.Nullary.Decidable.Core as Dec
 
 private
   variable
@@ -57,12 +56,13 @@ module _ {a b} {A : Set a} {B : Set b} where
   from-inj₂ (inj₁ _) = _
   from-inj₂ (inj₂ x) = x
 
--- Conversion back and forth with Dec
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
 
-fromDec : Dec A → A ⊎ ¬ A
-fromDec ( true because  [p]) = inj₁ (invert  [p])
-fromDec (false because [¬p]) = inj₂ (invert [¬p])
+open Dec public using (fromDec; toDec)
 
-toDec : A ⊎ ¬ A → Dec A
-toDec (inj₁ p)  = yes p
-toDec (inj₂ ¬p) = no ¬p

src/Relation/Nullary/Decidable/Core.agda

@@ -16,7 +16,7 @@ open import Level using (Level; Lift)
 open import Data.Bool.Base using (Bool; T; false; true; not; _∧_; _∨_)
 open import Data.Unit.Polymorphic.Base using (⊤)
 open import Data.Product.Base using (_×_)
-open import Data.Sum.Base using (_⊎_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; const; _$_; flip)
 open import Relation.Nullary.Recomputable as Recomputable hiding (recompute-constant)
 open import Relation.Nullary.Reflects as Reflects hiding (recompute; recompute-constant)
@@ -103,6 +103,17 @@ _→-dec_ : Dec A → Dec B → Dec (A → B)
 does  (a? →-dec b?) = not (does a?) ∨ does b?
 proof (a? →-dec b?) = proof a? →-reflects proof b?
 
+------------------------------------------------------------------------
+-- Relationship with Sum
+
+toSum : Dec A → A ⊎ ¬ A
+toSum ( true because  [p]) = inj₁ (invert  [p])
+toSum (false because [¬p]) = inj₂ (invert [¬p])
+
+fromSum : A ⊎ ¬ A → Dec A
+fromSum (inj₁ p)  = yes p
+fromSum (inj₂ ¬p) = no ¬p
+
 ------------------------------------------------------------------------
 -- Relationship with booleans
 
@@ -201,3 +212,17 @@ excluded-middle = ¬¬-excluded-middle
 "Warning: excluded-middle was deprecated in v2.0.
 Please use ¬¬-excluded-middle instead."
 #-}
+
+-- Version 2.1
+
+fromDec = toSum
+{-# WARNING_ON_USAGE fromDec
+"Warning: fromDec was deprecated in v2.1.
+Please use Relation.Nullary.Decidable.Core.toSum instead."
+#-}
+
+toDec = fromSum
+{-# WARNING_ON_USAGE toDec
+"Warning: toDec was deprecated in v2.1.
+Please use Relation.Nullary.Decidable.Core.fromSum instead."
+#-}