minor additions to Decidable and Reflects

CHANGELOG.md

@@ -682,6 +682,7 @@ Non-backwards compatible changes
   - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`.
   - `decidable-stable`, `excluded-middle` and `¬-drop-Dec` have been moved from `Relation.Nullary.Negation`
     to `Relation.Nullary.Decidable`.
+  - `excluded-middle` has been deprecated in favour of `¬¬-excluded-middle` 
   - `fromDec` and `toDec` have been moved from `Data.Sum.Base` to `Data.Sum`.
 
 ### Refactoring of the unindexed Functor/Applicative/Monad hierarchy
@@ -958,9 +959,6 @@ Non-backwards compatible changes
     lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x)
     lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
     ```
-  * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
-    `¬¬-excluded-middle`.
-
 Major improvements
 ------------------
 
@@ -1542,6 +1540,11 @@ Deprecated names
   invPreorder   ↦ converse-preorder
   ```
 
+* In `Relation.Nullary.Decidable.Core`:
+  ```
+  excluded-middle`  ↦  `¬¬-excluded-middle`
+  ```
+
 ### Renamed Data.Erased to Data.Irrelevant
 
 * This fixes the fact we had picked the wrong name originally. The erased modality
@@ -2406,8 +2409,8 @@ Additions to existing modules
   _!≢0    : NonZero (n !)
   _!*_!≢0 : NonZero (m ! * n !)
 
-  anyUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n)
-  allUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n)
+  anyUpTo? : ∀ (P? : Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n)
+  allUpTo? : ∀ (P? : Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n)
 
   n≤1⇒n≡0∨n≡1 : n ≤ 1 → n ≡ 0 ⊎ n ≡ 1
 
@@ -2921,6 +2924,16 @@ Additions to existing modules
   subst₂-removable : subst₂ _∼_ eq₁ eq₂ p ≅ p
   ```
 
+* Added new constructor for `Relation.Nullary.Decidable`
+  ```
+  T? : ∀ b → Dec (T b)
+  ```
+
+* Added new constructor for `Relation.Nullary.Reflects`
+  ```
+  T⁺ : ∀ b → Reflects (T b) b
+  ```
+
 * Added new definitions in `Relation.Unary`:
   ```
   _≐_  : Pred A ℓ₁ → Pred A ℓ₂ → Set _

README/Axiom.agda

@@ -31,7 +31,7 @@ private variable ℓ : Level
 -- The types for which `P` or `¬P` holds is called `Dec P` in the
 -- standard library (short for `Decidable`).
 
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable.Core using (Dec)
 
 -- The type of the proof of saying that excluded middle holds for
 -- all types at universe level ℓ is therefore:

README/Data/Trie/NonDependent.agda

@@ -64,7 +64,7 @@ open import Data.These       as These
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
 open import Relation.Nary
 open import Relation.Binary.Core using (Rel)
-open import Relation.Nullary.Decidable using (¬?)
+open import Relation.Nullary.Decidable.Core using (¬?)
 
 open import Data.Trie Char.<-strictTotalOrder
 open import Data.Tree.AVL.Value

README/Design/Decidability.agda

@@ -8,7 +8,7 @@
 
 module README.Design.Decidability where
 
-open import Data.Bool
+open import Data.Bool.Base
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Properties using (∷-injective)
 open import Data.Nat
@@ -43,7 +43,7 @@ ex₂ true  = ofʸ tt
 ------------------------------------------------------------------------
 -- Dec
 
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core
 
 -- A proof of `Dec P` is a proof of `Reflects P b` for some `b`.
 -- `Dec P` is declared as a record, with fields:

README/Foreign/Haskell.agda

@@ -24,7 +24,7 @@ open import Data.List.Base as List using (List; _∷_; []; takeWhile; dropWhile)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Product.Base using (_×_; _,_)
 open import Function
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core using (¬?)
 
 import Foreign.Haskell as FFI
 open import Foreign.Haskell.Coerce

README/Text/Regex.agda

@@ -12,8 +12,7 @@ open import Data.Bool using (true; false)
 open import Data.List.Base using (_∷_; [])
 open import Data.String
 open import Function.Base using () renaming (_$′_ to _$_)
-open import Relation.Nullary.Decidable using (yes)
-open import Relation.Nullary.Decidable using (True; False; from-yes)
+open import Relation.Nullary.Decidable.Core using (yes; True; False; from-yes)
 
 -- Our library available via the Text.Regex module is safe but it works on
 -- lists of characters.

src/Algebra/Construct/LexProduct/Inner.agda

@@ -12,8 +12,8 @@ open import Data.Product.Base using (_×_; _,_; swap; map; uncurry′)
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary.Decidable using (does; yes; no)
-open import Relation.Nullary.Negation
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
+open import Relation.Nullary.Negation.Core
   using (contradiction; contradiction₂)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 

src/Algebra/Properties/CancellativeCommutativeSemiring.agda

@@ -10,8 +10,8 @@ open import Algebra using (CancellativeCommutativeSemiring)
 open import Algebra.Definitions using (AlmostRightCancellative)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 module Algebra.Properties.CancellativeCommutativeSemiring
   {a ℓ} (R : CancellativeCommutativeSemiring a ℓ)

src/Algebra/Solver/CommutativeMonoid.agda

@@ -28,7 +28,7 @@ import Relation.Nullary.Decidable as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable.Core using (Dec)
 
 open CommutativeMonoid M
 open EqReasoning setoid

src/Algebra/Solver/IdempotentCommutativeMonoid.agda

@@ -26,7 +26,7 @@ import Relation.Nullary.Decidable            as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
 open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid)
-open import Relation.Nullary.Decidable using (Dec)
+open import Relation.Nullary.Decidable.Core using (Dec)
 
 module Algebra.Solver.IdempotentCommutativeMonoid
   {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where

src/Algebra/Solver/Monoid.agda

@@ -24,8 +24,7 @@ open import Relation.Binary.Definitions using (Decidable)
 
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.Reflection
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core using (map′)
 
 open Monoid M
 open import Relation.Binary.Reasoning.Setoid setoid
@@ -115,7 +114,7 @@ open module R = Relation.Binary.Reflection
 infix 5 _≟_
 
 _≟_ : ∀ {n} → Decidable {A = Normal n} _≡_
-nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
+nf₁ ≟ nf₂ = map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
   where open ListEq Fin._≟_
 
 -- We can also give a sound, but not necessarily complete, procedure

src/Algebra/Solver/Ring.agda

@@ -39,7 +39,7 @@ open import Algebra.Morphism
 open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧′)
 open import Algebra.Properties.Semiring.Exp semiring
 
-open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 open import Relation.Binary.Reasoning.Setoid setoid
 import Relation.Binary.PropositionalEquality.Core as PropEq
 import Relation.Binary.Reflection as Reflection

src/Axiom/DoubleNegationElimination.agda

@@ -12,7 +12,7 @@ open import Axiom.ExcludedMiddle
 open import Level
 open import Relation.Nullary
 open import Relation.Nullary.Negation
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core
 
 ------------------------------------------------------------------------
 -- Definition

src/Codata/Musical/Colist.agda

@@ -35,9 +35,8 @@ import Relation.Binary.Reasoning.Preorder as PreR
 import Relation.Binary.Reasoning.PartialOrder as POR
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary
 open import Relation.Nullary.Negation
-open import Relation.Nullary.Decidable using (¬¬-excluded-middle)
+open import Relation.Nullary.Decidable.Core using (Dec; _because_; ¬¬-excluded-middle)
 open import Relation.Unary using (Pred)
 
 private

src/Codata/Sized/Cofin/Literals.agda

@@ -13,7 +13,7 @@ open import Agda.Builtin.FromNat
 open import Codata.Sized.Conat
 open import Codata.Sized.Conat.Properties
 open import Codata.Sized.Cofin
-open import Relation.Nullary.Decidable
+open import Relation.Nullary.Decidable.Core using (True; toWitness)
 
 number : ∀ n → Number (Cofin n)
 number n = record

src/Codata/Sized/Conat/Properties.agda

@@ -15,7 +15,7 @@ open import Codata.Sized.Conat
 open import Codata.Sized.Conat.Bisimilarity
 open import Function.Base using (_∋_)
 open import Relation.Nullary
-open import Relation.Nullary.Decidable using (map′)
+open import Relation.Nullary.Decidable.Core using (map′)
 open import Relation.Binary.Definitions using (Decidable)
 
 private

src/Data/Bool.agda

@@ -8,9 +8,6 @@
 
 module Data.Bool where
 
-open import Relation.Nullary
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
-
 ------------------------------------------------------------------------
 -- The boolean type and some operations
 

src/Data/Bool/Properties.agda

@@ -28,8 +28,7 @@ open import Relation.Binary.Definitions
   using (Decidable; Reflexive; Transitive; Antisymmetric; Minimum; Maximum; Total; Irrelevant; Irreflexive; Asymmetric; Trans; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
 open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
-open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
-open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no)
+open import Relation.Nullary.Decidable.Core as Dec using (True; yes; no)
 import Relation.Unary as U
 
 open import Algebra.Definitions {A = Bool} _≡_
@@ -759,9 +758,7 @@ T-irrelevant : U.Irrelevant T
 T-irrelevant {true}  _  _  = refl
 
 T? : U.Decidable T
-does  (T? b) = b
-proof (T? true ) = ofʸ _
-proof (T? false) = ofⁿ λ()
+T? = Dec.T?
 
 T?-diag : ∀ b → T b → True (T? b)
 T?-diag true  _ = _

src/Data/Char/Properties.agda

@@ -16,7 +16,7 @@ open import Data.Product.Base using (_,_)
 
 open import Function.Base
 open import Relation.Nullary using (¬_; yes; no)
-open import Relation.Nullary.Decidable using (map′; isYes)
+open import Relation.Nullary.Decidable.Core using (map′; isYes)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder; Preorder; Poset; DecPoset)

src/Data/Digit.agda

@@ -19,7 +19,7 @@ open import Data.Product.Base using (∃; _,_)
 open import Data.Vec.Base as Vec using (Vec; _∷_; [])
 open import Data.Nat.DivMod
 open import Data.Nat.Induction
-open import Relation.Nullary.Decidable using (True; does; toWitness)
+open import Relation.Nullary.Decidable.Core using (True; does; toWitness)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 open import Function.Base using (_$_)

src/Data/Digit/Properties.agda

@@ -15,7 +15,7 @@ open import Data.Product.Base using (_,_; proj₁)
 open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
 import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
 open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
-open import Relation.Nullary.Decidable using (True; from-yes; ¬?)
+open import Relation.Nullary.Decidable.Core using (True; from-yes; ¬?)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Function.Base using (_∘_)
 

src/Data/Fin/Base.agda

@@ -17,11 +17,10 @@ open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
-open import Relation.Nullary.Negation.Core using (contradiction)
-open import Relation.Nullary.Decidable.Core using (yes; no; True; toWitness)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
 open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)
+open import Relation.Nullary.Negation.Core using (contradiction)
 
 private
   variable

src/Data/Fin/Induction.agda

@@ -31,8 +31,8 @@ import Relation.Binary.Construct.NonStrictToStrict as ToStrict
 import Relation.Binary.Construct.On as On
 open import Relation.Binary.Definitions using (Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Unary using (Pred)
 
 module Data.Fin.Induction where

src/Data/Fin/Literals.agda

@@ -9,12 +9,12 @@
 module Data.Fin.Literals where
 
 open import Agda.Builtin.FromNat
-open import Data.Nat using (suc; _≤?_)
+open import Data.Nat using (_<?_)
 open import Data.Fin using (Fin ; #_)
-open import Relation.Nullary.Decidable using (True)
+open import Relation.Nullary.Decidable.Core using (True)
 
 number : ∀ n → Number (Fin n)
 number n = record
-  { Constraint = λ m → True (suc m ≤? n)
+  { Constraint = λ m → True (m <? n)
   ; fromNat    = λ m {{pr}} → (# m) {n} {pr}
   }

src/Data/Fin/Properties.agda

@@ -43,10 +43,11 @@ open import Relation.Binary.Structures
   using (IsDecEquivalence; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning)
-open import Relation.Nullary
-  using (Reflects; ofʸ; ofⁿ; Dec; _because_; does; proof; yes; no; ¬_; _×-dec_; _⊎-dec_; contradiction)
-open import Relation.Nullary.Reflects
-open import Relation.Nullary.Decidable as Dec using (map′)
+open import Relation.Nullary.Decidable.Core
+  using (Dec; _because_; does; yes; no; _×-dec_; _⊎-dec_; map′)
+open import Relation.Nullary.Decidable using (via-injection)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
 open import Relation.Unary.Properties using (U?)
@@ -952,7 +953,7 @@ decFinSubset {suc n} {P = P} {Q} Q? P?
 
 any? : ∀ {p} {P : Pred (Fin n) p} → Decidable P → Dec (∃ P)
 any? {zero}  {P = _} P? = no λ { (() , _) }
-any? {suc n} {P = P} P? = Dec.map ⊎⇔∃ (P? zero ⊎-dec any? (P? ∘ suc))
+any? {suc n} {P = P} P? = map′ [ ∃-here , ∃-there ] ∃-toSum (P? zero ⊎-dec any? (P? ∘ suc))
 
 all? : ∀ {p} {P : Pred (Fin n) p} → Decidable P → Dec (∀ f → P f)
 all? P? = map′ (λ ∀p f → ∀p tt) (λ ∀p {x} _ → ∀p x)
@@ -1052,7 +1053,7 @@ module _ {ℓ} {S : Setoid a ℓ} (inj : Injection S (≡-setoid n)) where
   open Setoid S
 
   inj⇒≟ : B.Decidable _≈_
-  inj⇒≟ = Dec.via-injection inj _≟_
+  inj⇒≟ = via-injection inj _≟_
 
   inj⇒decSetoid : DecSetoid a ℓ
   inj⇒decSetoid = record

src/Data/Fin/Show.agda

@@ -14,8 +14,7 @@ open import Data.Nat as ℕ using (ℕ; _≤?_; _<?_)
 import Data.Nat.Show as ℕ using (show; readMaybe)
 open import Data.String.Base using (String)
 open import Function.Base
-open import Relation.Nullary.Decidable using (yes; no)
-open import Relation.Nullary.Decidable using (True)
+open import Relation.Nullary.Decidable.Core using (yes; no; True)
 
 show : ∀ {n} → Fin n → String
 show = ℕ.show ∘′ toℕ