agda · MatthewDaggitt · Oct 30, 2022 · Oct 25, 2022 · Oct 25, 2022 · Oct 30, 2022
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -534,6 +534,16 @@ Non-backwards compatible changes
 
 * Backwards compatibility has been maintained, as `Relation.Nullary` still re-exports these publicly.
 
+* The modules:
+  ```
+  Relation.Nullary.Product
+  Relation.Nullary.Sum
+  Relation.Nullary.Implication
+  ```
+  have been deprecated and their contents moved to `Relation.Nullary.(Negation/Reflects/Decidable)`
+  however all their contents is re-exported by `Relation.Nullary` which is the easiest way to access
+  it now.
+
 * In order to facilitate this reorganisation the following breaking moves have occured:
   - `¬?` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Decidable.Core`
   - `¬-reflects` has been moved from `Relation.Nullary.Negation.Core` to `Relation.Nullary.Reflects`.

diff --git a/README/Axiom.agda b/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 using (Dec)
+open import Relation.Nullary.Decidable using (Dec)
 
 -- The type of the proof of saying that excluded middle holds for
 -- all types at universe level ℓ is therefore:

diff --git a/README/Data/List/Relation/Binary/Pointwise.agda b/README/Data/List/Relation/Binary/Pointwise.agda
@@ -10,7 +10,7 @@ open import Data.Nat using (ℕ; _<_; s≤s; z≤n)
 open import Data.List using (List; []; _∷_; length)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong; setoid)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 ------------------------------------------------------------------------
 -- Pointwise

diff --git a/README/Design/Decidability.agda b/README/Design/Decidability.agda
@@ -8,13 +8,6 @@
 
 module README.Design.Decidability where
 
--- Reflects and Dec are defined in Relation.Nullary, and operations on them can
--- be found in Relation.Nullary.Reflects and Relation.Nullary.Decidable.
-
-open import Relation.Nullary as Nullary
-open import Relation.Nullary.Reflects
-open import Relation.Nullary.Decidable
-
 open import Data.Bool
 open import Data.List
 open import Data.List.Properties using (∷-injective)
@@ -25,7 +18,11 @@ open import Data.Unit
 open import Function
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nary
-open import Relation.Nullary.Product
+
+------------------------------------------------------------------------
+-- Reflects
+
+open import Relation.Nullary.Reflects
 
 infix 4 _≟₀_ _≟₁_ _≟₂_
 
@@ -43,6 +40,11 @@ ex₂ : (b : Bool) → Reflects (T b) b
 ex₂ false = ofⁿ id
 ex₂ true  = ofʸ tt
 
+------------------------------------------------------------------------
+-- Dec
+
+open import Relation.Nullary.Decidable
+
 -- A proof of `Dec P` is a proof of `Reflects P b` for some `b`.
 -- `Dec P` is declared as a record, with fields:
 --   does : Bool

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

diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda
@@ -22,7 +22,7 @@ open import Algebra.Definitions _≈_ using (Invertible)
 open import Algebra.Structures _≈_ using (IsCommutativeRing)
 open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation)
 open import Relation.Binary.Definitions using (Tight)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 import Relation.Binary.Properties.ApartnessRelation as AR
 
 

diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda
@@ -11,7 +11,7 @@ module Algebra.Bundles.Raw where
 open import Algebra.Core
 open import Relation.Binary.Core using (Rel)
 open import Level using (suc; _⊔_)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 ------------------------------------------------------------------------
 -- Raw bundles with 1 binary operation

diff --git a/src/Algebra/Construct/LexProduct/Base.agda b/src/Algebra/Construct/LexProduct/Base.agda
@@ -11,7 +11,7 @@ open import Data.Bool.Base using (true; false)
 open import Data.Product using (_×_; _,_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary using (does; yes; no)
+open import Relation.Nullary.Decidable using (does; yes; no)
 
 module Algebra.Construct.LexProduct.Base
   {a b ℓ} {A : Set a} {B : Set b}

diff --git a/src/Algebra/Construct/LexProduct/Inner.agda b/src/Algebra/Construct/LexProduct/Inner.agda
@@ -12,7 +12,7 @@ open import Data.Product 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 using (does; yes; no)
+open import Relation.Nullary.Decidable using (does; yes; no)
 open import Relation.Nullary.Negation
   using (contradiction; contradiction₂)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning

diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
@@ -16,7 +16,7 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary.Core
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 module Algebra.Definitions
   {a ℓ} {A : Set a}   -- The underlying set

diff --git a/src/Algebra/Definitions/RawMagma.agda b/src/Algebra/Definitions/RawMagma.agda
@@ -14,7 +14,7 @@ open import Algebra.Bundles using (RawMagma)
 open import Data.Product using (_×_; ∃)
 open import Level using (_⊔_)
 open import Relation.Binary.Core
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 module Algebra.Definitions.RawMagma
   {a ℓ} (M : RawMagma a ℓ)

diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
@@ -10,7 +10,7 @@ open import Algebra using (CancellativeCommutativeSemiring)
 open import Algebra.Definitions using (AlmostRightCancellative)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Relation.Binary using (Decidable)
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 
 module Algebra.Properties.CancellativeCommutativeSemiring

diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/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 as P using (_≡_; decSetoid)
-open import Relation.Nullary using (Dec)
+open import Relation.Nullary.Decidable using (Dec)
 
 open CommutativeMonoid M
 open EqReasoning setoid

diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/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 using (Dec)
+open import Relation.Nullary.Decidable using (Dec)
 
 module Algebra.Solver.IdempotentCommutativeMonoid
   {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where

diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda
@@ -40,7 +40,7 @@ open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧′)
 open import Algebra.Properties.Semiring.Exp semiring
 
 open import Relation.Binary
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Binary.Reasoning.Setoid setoid
 import Relation.Binary.PropositionalEquality as PropEq
 import Relation.Binary.Reflection as Reflection

diff --git a/src/Data/Digit.agda b/src/Data/Digit.agda
@@ -19,7 +19,7 @@ open import Data.Product
 open import Data.Vec.Base as Vec using (Vec; _∷_; [])
 open import Data.Nat.DivMod
 open import Data.Nat.Induction
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 open import Relation.Nullary.Decidable
 open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)

diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
@@ -18,7 +18,7 @@ open import Data.Product 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 using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Nullary.Decidable.Core using (True; toWitness)
 open import Relation.Binary.Core

diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda
@@ -29,7 +29,7 @@ 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 using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Unary using (Pred)
 

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
@@ -37,13 +37,10 @@ open import Level using (Level)
 open import Relation.Binary as B hiding (Decidable; _⇔_)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst; _≗_; module ≡-Reasoning)
-open import Relation.Nullary.Decidable as Dec using (map′)
-open import Relation.Nullary.Reflects
-open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Nullary
-  using (Reflects; ofʸ; ofⁿ; Dec; _because_; does; proof; yes; no; ¬_)
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Nullary.Sum using (_⊎-dec_)
+  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.Unary as U
   using (U; Pred; Decidable; _⊆_; Satisfiable; Universal)
 open import Relation.Unary.Properties using (U?)

diff --git a/src/Data/Fin/Show.agda b/src/Data/Fin/Show.agda
@@ -14,7 +14,7 @@ open import Data.Nat as ℕ using (ℕ; _≤?_; _<?_)
 import Data.Nat.Show as ℕ
 open import Data.String.Base using (String)
 open import Function.Base
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable using (True)
 
 show : ∀ {n} → Fin n → String

diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
@@ -32,10 +32,8 @@ open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level)
 open import Relation.Binary as B hiding (Decidable; _⇔_)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (Dec; yes; no)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Sum using (_⊎-dec_)
 open import Relation.Unary using (Pred; Decidable; Satisfiable)
 
 private

diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda
@@ -20,7 +20,7 @@ open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Unary using (Pred)
 

diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda
@@ -24,7 +24,7 @@ open import Level
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 import Relation.Nullary.Decidable as DEC
 
 ------------------------------------------------------------------------

diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
@@ -22,7 +22,7 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base using (id; _∘_ ; _∘′_; _∘₂_; const; flip)
 open import Level using (Level)
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 open import Relation.Nullary.Decidable using (¬?)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Unary.Properties using (∁?)

diff --git a/src/Data/List/Fresh/Relation/Unary/All.agda b/src/Data/List/Fresh/Relation/Unary/All.agda
@@ -11,9 +11,7 @@ module Data.List.Fresh.Relation.Unary.All where
 open import Level using (Level; _⊔_; Lift)
 open import Data.Product using (_×_; _,_; proj₁; uncurry)
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_)
 open import Relation.Unary  as U
 open import Relation.Binary as B using (Rel)
 

diff --git a/src/Data/List/Fresh/Relation/Unary/Any.agda b/src/Data/List/Fresh/Relation/Unary/Any.agda
@@ -13,9 +13,8 @@ open import Data.Empty
 open import Data.Product using (∃; _,_; -,_)
 open import Data.Sum.Base using (_⊎_; [_,_]′; inj₁; inj₂)
 open import Function.Bundles using (_⇔_; mk⇔)
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_)
 open import Relation.Unary  as U
 open import Relation.Binary as B using (Rel)
 

diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
@@ -16,7 +16,7 @@ open import Data.List.Relation.Unary.Any
   using (Any; index; map; here; there)
 open import Data.Product as Prod using (∃; _×_; _,_)
 open import Relation.Unary using (Pred)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 open Setoid S renaming (Carrier to A)
 

diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
@@ -23,7 +23,7 @@ open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl)
 open import Relation.Unary using (Pred; Decidable; U; ∅)
 open import Relation.Unary.Properties using (U?; ∅?)
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 
 private
   variable

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
@@ -36,10 +36,8 @@ import Relation.Binary.Reasoning.Setoid as EqR
 open import Relation.Binary.PropositionalEquality as P hiding ([_])
 open import Relation.Binary as B using (Rel)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction)
+open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_)
 open import Relation.Unary using (Pred; Decidable; ∁)
 open import Relation.Unary.Properties using (∁?)
 

diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid.agda
@@ -11,7 +11,7 @@ open import Relation.Binary
 module Data.List.Relation.Binary.Disjoint.Setoid {c ℓ} (S : Setoid c ℓ) where
 
 open import Level using (_⊔_)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Function.Base using (_∘_)
 open import Data.List.Base using (List; []; [_]; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)

diff --git a/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
@@ -17,7 +17,7 @@ open import Data.List.Relation.Unary.Any.Properties using (++⁻)
 open import Data.Product using (_,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 ------------------------------------------------------------------------
 -- Relational properties

diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
@@ -17,10 +17,8 @@ import Data.Nat.Properties as ℕₚ
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (case_of_; _$′_)
 
-open import Relation.Nullary using (¬_; yes; no; does)
-open import Relation.Nullary.Decidable using (map′)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎-dec_)
+open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary using (REL; _⇒_; Decidable; Trans; Antisym)
 open import Relation.Binary.PropositionalEquality using (_≢_; refl; cong)

diff --git a/src/Data/List/Relation/Binary/Lex.agda b/src/Data/List/Relation/Binary/Lex.agda
@@ -16,10 +16,9 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (_∘_; flip; id)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (_⊔_)
-open import Relation.Nullary using (Dec; yes; no; ¬_)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Decidable as Dec
+  using (Dec; yes; no; _×-dec_; _⊎-dec_)
 open import Relation.Binary hiding (_⇔_)
 open import Data.List.Relation.Binary.Pointwise.Base
    using (Pointwise; []; _∷_; head; tail)

diff --git a/src/Data/List/Relation/Binary/Lex/Core.agda b/src/Data/List/Relation/Binary/Lex/Core.agda
@@ -14,7 +14,7 @@ open import Data.Product using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Data.List.Base using (List; []; _∷_)
 open import Function.Base using (_∘_; flip; id)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.Core using (Rel)
 open import Data.List.Relation.Binary.Pointwise.Base
    using (Pointwise; []; _∷_; head; tail)

diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -38,7 +38,7 @@ open import Relation.Unary using (Pred; Decidable)
 open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
 open import Relation.Binary.PropositionalEquality as ≡
   using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_; inspect)
-open import Relation.Nullary using (yes; no; does)
+open import Relation.Nullary.Decidable using (yes; no; does)
 open import Relation.Nullary.Negation using (contradiction)
 
 private

diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda
@@ -23,9 +23,7 @@ open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Nat.Properties
 open import Level
 open import Relation.Nullary hiding (Irrelevant)
-open import Relation.Nullary.Negation.Core using (contradiction)
 import Relation.Nullary.Decidable as Dec using (map′)
-open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary renaming (Rel to Rel₂)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)