diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6c83ff0b49..5114b01558 100644
--- 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
index d22dfc0ca9..43805af9c5 100644
--- 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
index 6b0bc17e00..4932413ad4 100644
--- 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
index 610f5d1352..fe4b0583cd 100644
--- 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
index 7a23eb9928..5b4ce805c0 100644
--- 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
index e8a8a61b28..bf07ac14c1 100644
--- 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
index 2b55574f74..d793d558fe 100644
--- 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
index 6bc8027da8..0a0934ac9e 100644
--- 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
index 585e868961..d2312c7985 100644
--- 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
index 2552641544..c2a51fed69 100644
--- 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
index fd1db803b5..bf056f035b 100644
--- 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
index 081050800a..84dadf83f9 100644
--- 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
index fbf8527478..263800030d 100644
--- 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
index 2a58559d78..348d04d26b 100644
--- 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
index b379618ecd..c30e6e1c24 100644
--- 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
index d8c67ca730..a520b9f08d 100644
--- 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
index 93ea438156..a3b26cf7aa 100644
--- 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
index 954aac6f48..d86423bda3 100644
--- 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
index 07c7ae982b..cb19ae7ab4 100644
--- 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
index f9816e4900..bf101ee99c 100644
--- 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
index a2863f672a..f075e4ed81 100644
--- 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
index 4432615c77..b195861192 100644
--- 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
index e544d6a62c..81b254ff25 100644
--- 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
index fb7e17fe28..83210e3803 100644
--- 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
index f44b28a291..22467bc508 100644
--- 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
index 480d011006..fae8cbc919 100644
--- 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
index e8476d9a44..53df8ee480 100644
--- 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
index 2d15005235..ae1e9cece5 100644
--- 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
index 5bc11aeef1..0e4e1b822d 100644
--- 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
index 7df1d76455..3c8c8a6aba 100644
--- 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
index 03669299c4..c55fc37ca3 100644
--- 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
index 48ebe35237..a6e74c18a6 100644
--- 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
index 419cc5d378..92a4c9168d 100644
--- 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
index 8de585e119..1155a2a7e1 100644
--- 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
index 01a286b2c5..fe2a4620ae 100644
--- 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
index a0ec61758c..cfe9509757 100644
--- 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 (_≡_)
diff --git a/src/Data/List/Relation/Binary/Pointwise/Properties.agda b/src/Data/List/Relation/Binary/Pointwise/Properties.agda
index c7f59fd1a6..28154f908d 100644
--- a/src/Data/List/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/List/Relation/Binary/Pointwise/Properties.agda
@@ -14,8 +14,7 @@ open import Level
 open import Relation.Binary.Core using (REL; _⇒_)
 open import Relation.Binary.Definitions
 import Relation.Binary.PropositionalEquality as P
-open import Relation.Nullary using (yes; no)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary using (yes; no; _×-dec_)
 import Relation.Nullary.Decidable as Dec
 
 open import Data.List.Relation.Binary.Pointwise.Base
diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
index cb3b66adc3..7f1c76a50d 100644
--- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
@@ -20,11 +20,10 @@ open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix hiding (Pre
 open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (suc-injective)
 open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂; uncurry)
-open import Function
+open import Function.Base
 
-open import Relation.Nullary using (yes; no; ¬_; _because_)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no; _because_)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index c9241680aa..46b8ae260d 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -22,7 +22,7 @@ open import Function.Bundles using (_⇔_; _⤖_)
 open import Level
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
 open import Relation.Unary using (Pred; Decidable; Irrelevant)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable using (¬?)
 
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
diff --git a/src/Data/List/Relation/Binary/Subset/Setoid.agda b/src/Data/List/Relation/Binary/Subset/Setoid.agda
index e62a6285e7..9a972d9301 100644
--- a/src/Data/List/Relation/Binary/Subset/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Subset/Setoid.agda
@@ -15,7 +15,7 @@ open import Data.List.Base using (List)
 open import Data.List.Membership.Setoid S using (_∈_)
 open import Function.Base using (flip)
 open import Level using (_⊔_)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 open Setoid S renaming (Carrier to A)
 
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
index 9ee8241d6c..f489a9dfb5 100644
--- a/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
@@ -14,7 +14,7 @@ module Data.List.Relation.Ternary.Interleaving.Setoid.Properties
 open import Data.List.Base using (List; []; _∷_; filter; _++_)
 open import Data.Bool.Base using (true; false)
 open import Relation.Unary using (Decidable)
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 open import Relation.Nullary.Decidable using (¬?)
 open import Function
 
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index 33f71dcca5..a878d01dd3 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -22,7 +22,6 @@ open import Function
 open import Level
 open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
 open import Relation.Unary hiding (_∈_)
 open import Relation.Binary using (Setoid; _Respects_)
 open import Relation.Binary.PropositionalEquality as P
diff --git a/src/Data/List/Relation/Unary/AllPairs.agda b/src/Data/List/Relation/Unary/AllPairs.agda
index a320f03d73..c99767cc52 100644
--- a/src/Data/List/Relation/Unary/AllPairs.agda
+++ b/src/Data/List/Relation/Unary/AllPairs.agda
@@ -20,9 +20,7 @@ open import Relation.Binary as B using (Rel; _⇒_)
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
-open import Relation.Nullary using (yes; no)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no)
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
index 0a588cc0b1..0044917b50 100644
--- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda
+++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
@@ -22,7 +22,7 @@ open import Level using (Level)
 open import Relation.Binary using (Rel; DecSetoid)
 open import Relation.Binary.PropositionalEquality using (_≢_)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda
index 02f7219229..f56e46dd6f 100644
--- a/src/Data/List/Relation/Unary/Any.agda
+++ b/src/Data/List/Relation/Unary/Any.agda
@@ -14,10 +14,9 @@ open import Data.List.Base as List using (List; []; [_]; _∷_)
 open import Data.Product as Prod using (∃; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary using (¬_; yes; no)
+open import Relation.Nullary using (¬_; yes; no; _⊎-dec_)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Sum using (_⊎-dec_)
 open import Relation.Unary hiding (_∈_)
 
 private
diff --git a/src/Data/List/Relation/Unary/Grouped.agda b/src/Data/List/Relation/Unary/Grouped.agda
index eecdb1f75f..c1c9b75994 100644
--- a/src/Data/List/Relation/Unary/Grouped.agda
+++ b/src/Data/List/Relation/Unary/Grouped.agda
@@ -14,24 +14,37 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Product using (_×_; _,_)
 open import Relation.Binary as B using (REL; Rel)
 open import Relation.Unary as U using (Pred)
-open import Relation.Nullary using (¬_; yes)
-open import Relation.Nullary.Decidable as Dec using (¬?)
-open import Relation.Nullary.Sum using (_⊎-dec_)
-open import Relation.Nullary.Product using (_×-dec_)
-open import Level using (_⊔_)
+open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Decidable as Dec using (yes; ¬?; _⊎-dec_; _×-dec_)
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    a ℓ : Level
+    A : Set a
+    x y : A
+    xs : List A
+
+------------------------------------------------------------------------
+-- Definition
 
 infixr 5 _∷≉_ _∷≈_
 
-data Grouped {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) : Pred (List A) (a ⊔ ℓ) where
+data Grouped {A : Set a} (_≈_ : Rel A ℓ) : Pred (List A) (a ⊔ ℓ) where
   [] : Grouped _≈_ []
-  _∷≉_ : ∀ {x xs} → All (λ y → ¬ (x ≈ y)) xs → Grouped _≈_ xs → Grouped _≈_ (x ∷ xs)
-  _∷≈_ : ∀ {x y xs} → x ≈ y → Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs)
+  _∷≉_ : All (λ y → ¬ (x ≈ y)) xs → Grouped _≈_ xs → Grouped _≈_ (x ∷ xs)
+  _∷≈_ : x ≈ y → Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs)
+
+------------------------------------------------------------------------
+-- Basic properties
+
+module _ {_≈_ : Rel A ℓ} where
 
-module _ {a ℓ} {A : Set a} {_≈_ : Rel A ℓ} where
   grouped? : B.Decidable _≈_ → U.Decidable (Grouped _≈_)
   grouped? _≟_ [] = yes []
   grouped? _≟_ (x ∷ []) = yes ([] ∷≉ [])
-  grouped? _≟_ (x ∷ y ∷ xs) = Dec.map′ from to ((x ≟ y ⊎-dec all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs)))
+  grouped? _≟_ (x ∷ y ∷ xs) =
+    Dec.map′ from to ((x ≟ y ⊎-dec all? (λ z → ¬? (x ≟ z)) (y ∷ xs)) ×-dec (grouped? _≟_ (y ∷ xs)))
     where
     from : ((x ≈ y) ⊎ All (λ z → ¬ (x ≈ z)) (y ∷ xs)) × Grouped _≈_ (y ∷ xs) → Grouped _≈_ (x ∷ y ∷ xs)
     from (inj₁ x≈y          , grouped[y∷xs]) = x≈y          ∷≈ grouped[y∷xs]
diff --git a/src/Data/List/Relation/Unary/Linked.agda b/src/Data/List/Relation/Unary/Linked.agda
index dca6c056dd..6a1440203c 100644
--- a/src/Data/List/Relation/Unary/Linked.agda
+++ b/src/Data/List/Relation/Unary/Linked.agda
@@ -20,9 +20,7 @@ open import Relation.Binary as B using (Rel; _⇒_)
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
-open import Relation.Nullary using (yes; no)
-open import Relation.Nullary.Decidable as Dec using (map′)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/Linked/Properties.agda b/src/Data/List/Relation/Unary/Linked/Properties.agda
index 494e710f84..6d6341489b 100644
--- a/src/Data/List/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/List/Relation/Unary/Linked/Properties.agda
@@ -25,7 +25,7 @@ open import Function.Base using (_∘_; flip; _on_)
 open import Relation.Binary using (Rel; Transitive; DecSetoid)
 open import Relation.Binary.PropositionalEquality using (_≢_)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary using (yes; no; does)
+open import Relation.Nullary.Decidable using (yes; no; does)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
index 47b101128a..66bbbeccca 100644
--- a/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
+++ b/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
@@ -22,7 +22,7 @@ open import Level using (Level)
 open import Relation.Binary hiding (Decidable)
 import Relation.Binary.Properties.TotalOrder as TotalOrderProperties
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 private
   variable
     a b p ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level
diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
index c9ac3bff73..da257037a3 100644
--- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
@@ -25,7 +25,7 @@ open import Relation.Binary using (Rel; Setoid)
 open import Relation.Binary.PropositionalEquality
   using (refl; _≡_; _≢_; sym; setoid)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/Unique/Setoid.agda b/src/Data/List/Relation/Unary/Unique/Setoid.agda
index b287d87b4e..fe52fe693e 100644
--- a/src/Data/List/Relation/Unary/Unique/Setoid.agda
+++ b/src/Data/List/Relation/Unary/Unique/Setoid.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary using (Rel; Setoid)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 module Data.List.Relation.Unary.Unique.Setoid {a ℓ} (S : Setoid a ℓ) where
 
diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
index e182b43363..b766a00a0e 100644
--- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
@@ -26,7 +26,7 @@ open import Level using (Level)
 open import Relation.Binary using (Rel; Setoid)
 open import Relation.Binary.PropositionalEquality using (_≡_)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (contraposition)
 
 private
diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda
index d91e11c5b4..0dc5ded0fb 100644
--- a/src/Data/List/Sort/MergeSort.agda
+++ b/src/Data/List/Sort/MergeSort.agda
@@ -20,14 +20,14 @@ import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Binary.Permutation.Propositional
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm
 open import Data.Maybe.Base using (just)
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 open import Data.Nat using (_<_; _>_; z<s; s<s)
 open import Data.Nat.Induction
 open import Data.Nat.Properties using (m<n⇒m<1+n)
 open import Data.Product as Prod using (_,_)
 open import Function.Base using (_∘_)
 open import Relation.Binary using (DecTotalOrder)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 module Data.List.Sort.MergeSort
   {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where
diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda
index 2ade049d6e..0788c0517f 100644
--- a/src/Data/Maybe/Properties.agda
+++ b/src/Data/Maybe/Properties.agda
@@ -18,7 +18,7 @@ open import Function
 open import Level using (Level)
 open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable using (map′)
 
 private
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index 6c6a7fa062..4ec0c4fe84 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -18,7 +18,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/Nat/Binary/Base.agda b/src/Data/Nat/Binary/Base.agda
index 6850264c09..cf6bd8a361 100644
--- a/src/Data/Nat/Binary/Base.agda
+++ b/src/Data/Nat/Binary/Base.agda
@@ -21,7 +21,7 @@ open import Function.Base using (_on_)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Data/Nat/Combinatorics/Specification.agda b/src/Data/Nat/Combinatorics/Specification.agda
index 57c29b233b..cb78973035 100644
--- a/src/Data/Nat/Combinatorics/Specification.agda
+++ b/src/Data/Nat/Combinatorics/Specification.agda
@@ -19,7 +19,7 @@ open import Data.Nat.Combinatorics.Base
 open import Data.Sum using (inj₁; inj₂)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; trans; _≢_)
-open import Relation.Nullary using (yes; no; does)
+open import Relation.Nullary.Decidable using (yes; no; does)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.PropositionalEquality
   using (subst; refl; sym; cong; cong₂)
diff --git a/src/Data/Nat/DivMod.agda b/src/Data/Nat/DivMod.agda
index 622b2f8b92..40cf47b1a9 100644
--- a/src/Data/Nat/DivMod.agda
+++ b/src/Data/Nat/DivMod.agda
@@ -19,7 +19,7 @@ open import Data.Nat.Induction
 open import Data.Nat.Properties
 open import Function using (_$_)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable using (False; toWitnessFalse)
 
 import Algebra.Properties.CommutativeSemigroup *-commutativeSemigroup as *-CS
diff --git a/src/Data/Nat/DivMod/Core.agda b/src/Data/Nat/DivMod/Core.agda
index 61d225f39a..3e4bbac346 100644
--- a/src/Data/Nat/DivMod/Core.agda
+++ b/src/Data/Nat/DivMod/Core.agda
@@ -16,7 +16,7 @@ open import Data.Nat.Properties
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.Product using (_×_; _,_)
 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 ≤-Reasoning
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index 3dbb4a3933..7a1d26748c 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -17,7 +17,7 @@ open import Data.Unit using (tt)
 open import Function.Base
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (0ℓ)
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable as Dec using (False)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary
diff --git a/src/Data/Nat/Divisibility/Core.agda b/src/Data/Nat/Divisibility/Core.agda
index b16a7f8363..04f1289aa4 100644
--- a/src/Data/Nat/Divisibility/Core.agda
+++ b/src/Data/Nat/Divisibility/Core.agda
@@ -15,7 +15,7 @@ module Data.Nat.Divisibility.Core where
 open import Data.Nat.Base using (ℕ; _*_)
 open import Data.Nat.Properties
 open import Level using (0ℓ)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary using (Rel)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong₂; module ≡-Reasoning)
diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda
index d7748e12a0..dcd7cba6f1 100644
--- a/src/Data/Nat/GCD.agda
+++ b/src/Data/Nat/GCD.agda
@@ -23,7 +23,7 @@ open import Induction.Lexicographic using (_⊗_; [_⊗_])
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; subst; cong)
-open import Relation.Nullary using (Dec)
+open import Relation.Nullary.Decidable using (Dec)
 open import Relation.Nullary.Negation using (contradiction)
 import Relation.Nullary.Decidable as Dec
 
diff --git a/src/Data/Nat/InfinitelyOften.agda b/src/Data/Nat/InfinitelyOften.agda
index b966d60c8b..527e0c73fc 100644
--- a/src/Data/Nat/InfinitelyOften.agda
+++ b/src/Data/Nat/InfinitelyOften.agda
@@ -17,7 +17,7 @@ open import Data.Product as Prod hiding (map)
 open import Data.Sum hiding (map)
 open import Function
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (¬¬-Monad; call/cc)
 open import Relation.Unary using (Pred; _∪_; _⊆_)
 open RawMonad (¬¬-Monad {p = 0ℓ})
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index e2d93fc61d..ac0b2d3585 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -16,13 +16,12 @@ open import Data.Nat.Properties
 open import Data.Product
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (flip; _∘_; _∘′_)
-open import Relation.Nullary using (yes; no; ¬_)
-open import Relation.Nullary.Decidable as Dec using (from-yes; ¬?; decidable-stable)
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Nullary.Implication using (_→-dec_)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable as Dec
+  using (yes; no; from-yes; ¬?; decidable-stable; _×-dec_; _→-dec_)
+open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Unary using (Decidable)
-open import Relation.Binary.PropositionalEquality using (refl; sym; cong; subst)
+open import Relation.Binary.PropositionalEquality
+  using (refl; sym; cong; subst)
 
 private
   variable
diff --git a/src/Data/Product/Nary/NonDependent.agda b/src/Data/Product/Nary/NonDependent.agda
index e5fc523109..de390a5f2a 100644
--- a/src/Data/Product/Nary/NonDependent.agda
+++ b/src/Data/Product/Nary/NonDependent.agda
@@ -22,8 +22,7 @@ open import Data.Sum.Base using (_⊎_)
 open import Data.Nat.Base using (ℕ; zero; suc; pred)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Function.Base using (const; _∘′_; _∘_)
-open import Relation.Nullary
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable using (Dec; yes; no; _×-dec_)
 open import Relation.Binary using (Rel)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂)
 
diff --git a/src/Data/Product/Properties.agda b/src/Data/Product/Properties.agda
index 649c63715c..949667286b 100644
--- a/src/Data/Product/Properties.agda
+++ b/src/Data/Product/Properties.agda
@@ -14,9 +14,7 @@ open import Function
 open import Level using (Level)
 open import Relation.Binary using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary.Product
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no)
 
 private
   variable
diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index 0dccfc4216..0958e45883 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda
@@ -11,7 +11,7 @@
 
 module Data.Product.Relation.Binary.Lex.Strict where
 
-open import Data.Product
+open import Data.Product.Base
 open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
   using (Pointwise)
 open import Data.Sum.Base using (inj₁; inj₂; _-⊎-_; [_,_])
@@ -19,9 +19,7 @@ open import Data.Empty
 open import Function.Base
 open import Induction.WellFounded
 open import Level
-open import Relation.Nullary
-open import Relation.Nullary.Product
-open import Relation.Nullary.Sum
+open import Relation.Nullary.Decidable
 open import Relation.Binary
 open import Relation.Binary.Consequences
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
index e79933371f..56b6b37933 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
@@ -25,8 +25,7 @@ open import Function.LeftInverse as LeftInv
 open import Function.Related
 open import Function.Surjection as Surj
   using (Surjection; _↠_; module Surjection)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product
+open import Relation.Nullary.Decidable using (_×-dec_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 6826094088..3851b0601c 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -52,12 +52,9 @@ open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Morphism.Structures
 import Relation.Binary.Morphism.OrderMonomorphism as OrderMonomorphisms
-open import Relation.Nullary using (¬_; yes; no; recompute)
 open import Relation.Nullary.Decidable as Dec
-  using (True; False; fromWitness; fromWitnessFalse; toWitnessFalse)
-open import Relation.Nullary.Negation using (contradiction; contraposition)
-open import Relation.Nullary.Decidable as Dec using (True; fromWitness; map′)
-open import Relation.Nullary.Product using (_×-dec_)
+  using (True; False; fromWitness; fromWitnessFalse; toWitnessFalse; yes; no; recompute; map′; _×-dec_)
+open import Relation.Nullary.Negation using (¬_; contradiction; contraposition)
 
 open import Algebra.Definitions {A = ℚ} _≡_
 open import Algebra.Structures  {A = ℚ} _≡_
diff --git a/src/Data/Rational/Unnormalised/Base.agda b/src/Data/Rational/Unnormalised/Base.agda
index e146b809af..a1bf66fcbd 100644
--- a/src/Data/Rational/Unnormalised/Base.agda
+++ b/src/Data/Rational/Unnormalised/Base.agda
@@ -14,7 +14,7 @@ open import Data.Integer.Base as ℤ
   using (ℤ; +_; +0; +[1+_]; -[1+_]; +<+; +≤+)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Level using (0ℓ)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Unary using (Pred)
 open import Relation.Binary.Core using (Rel)
diff --git a/src/Data/Sign/Properties.agda b/src/Data/Sign/Properties.agda
index eb0d97227a..e9c278e676 100644
--- a/src/Data/Sign/Properties.agda
+++ b/src/Data/Sign/Properties.agda
@@ -17,7 +17,7 @@ open import Level using (0ℓ)
 open import Relation.Binary
   using (Decidable; DecidableEquality; Setoid; DecSetoid; IsDecEquivalence)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 
 open import Algebra.Structures {A = Sign} _≡_
 open import Algebra.Definitions {A = Sign} _≡_
diff --git a/src/Data/String.agda b/src/Data/String.agda
index dd3eea3a0b..b6986b50cd 100644
--- a/src/Data/String.agda
+++ b/src/Data/String.agda
@@ -24,7 +24,7 @@ import Data.Char.Properties as Char using (_≟_)
 open import Function
 open import Relation.Binary using (Rel)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 open import Relation.Unary using (Pred; Decidable)
 
 open import Data.List.Membership.DecPropositional Char._≟_
diff --git a/src/Data/String/Base.agda b/src/Data/String/Base.agda
index 2be9738d93..87f04c6862 100644
--- a/src/Data/String/Base.agda
+++ b/src/Data/String/Base.agda
@@ -23,7 +23,7 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 
 ------------------------------------------------------------------------
 -- From Agda.Builtin: type and renamed primitives
diff --git a/src/Data/String/Properties.agda b/src/Data/String/Properties.agda
index ddfce82e69..ed81788daa 100644
--- a/src/Data/String/Properties.agda
+++ b/src/Data/String/Properties.agda
@@ -15,7 +15,7 @@ import Data.List.Relation.Binary.Pointwise as Pointwise
 import Data.List.Relation.Binary.Lex.Strict as StrictLex
 open import Data.String.Base
 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 (map′; isYes)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core
diff --git a/src/Data/Sum/Properties.agda b/src/Data/Sum/Properties.agda
index 7042b8682f..8a632d28c5 100644
--- a/src/Data/Sum/Properties.agda
+++ b/src/Data/Sum/Properties.agda
@@ -14,7 +14,7 @@ open import Function
 open import Function.Bundles using (mk↔′)
 open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable using (map′)
 
 
diff --git a/src/Data/These/Properties.agda b/src/Data/These/Properties.agda
index 98ed00e697..55672ed63f 100644
--- a/src/Data/These/Properties.agda
+++ b/src/Data/These/Properties.agda
@@ -13,9 +13,7 @@ open import Data.These.Base
 open import Function.Base using (_∘_)
 open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (yes; no)
-open import Relation.Nullary.Decidable using (map′)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)
 
 ------------------------------------------------------------------------
 -- Equality
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
index 67baab339a..f2be362cb1 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
@@ -21,9 +21,7 @@ open import Function.Nary.NonDependent using (congₙ)
 open import Level using (Level; _⊔_)
 
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-open import Relation.Nullary using (Dec; yes)
-open import Relation.Nullary.Decidable using (map′)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable using (Dec; yes; map′; _×-dec_)
 open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant; _⊆_; _∪_)
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index 5ff87e7c14..4f6978faf5 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -18,9 +18,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (_∘′_; _∘_)
 open import Level using (Level; _⊔_)
 
-open import Relation.Nullary using (Dec; no)
-open import Relation.Nullary.Decidable using (map′)
-open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Decidable using (Dec; no; map′; _⊎-dec_)
 open import Relation.Unary
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index d358ccd01b..79dadda89a 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -21,7 +21,7 @@ open import Level using (Level)
 
 open import Relation.Binary using (_Respects_; tri<; tri≈; tri>)
 open import Relation.Unary using (Pred)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (contradiction)
 
 open import Data.Tree.AVL.Indexed sto as AVL
diff --git a/src/Data/Tree/AVL/Key.agda b/src/Data/Tree/AVL/Key.agda
index 77063c49d6..7a3ee66050 100644
--- a/src/Data/Tree/AVL/Key.agda
+++ b/src/Data/Tree/AVL/Key.agda
@@ -18,7 +18,7 @@ open import Data.Empty
 open import Data.Unit
 open import Data.Product
 open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Construct.Add.Extrema
   as AddExtremaToSet using (_±)
 import Relation.Binary.Construct.Add.Extrema.Equality
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index d25c2384c8..c7ea56174a 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -17,7 +17,7 @@ open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base using (const; _∘′_; id; _∘_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 open import Relation.Unary using (Pred; Decidable)
 
 private
diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
index 926627ed17..311b62bd31 100644
--- a/src/Data/Vec/Functional/Properties.agda
+++ b/src/Data/Vec/Functional/Properties.agda
@@ -23,9 +23,8 @@ open import Function.Base
 open import Level using (Level)
 open import Relation.Binary as B
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary using (Dec; does; yes; no)
-open import Relation.Nullary.Decidable using (map′)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable
+  using (Dec; does; yes; no; map′; _×-dec_)
 
 import Data.Fin.Properties as Finₚ
 
diff --git a/src/Data/Vec/Membership/DecSetoid.agda b/src/Data/Vec/Membership/DecSetoid.agda
index c1b4e1e916..a9ff2d58ea 100644
--- a/src/Data/Vec/Membership/DecSetoid.agda
+++ b/src/Data/Vec/Membership/DecSetoid.agda
@@ -12,7 +12,7 @@ module Data.Vec.Membership.DecSetoid {c ℓ} (DS : DecSetoid c ℓ) where
 
 open import Data.Vec.Base using (Vec)
 open import Data.Vec.Relation.Unary.Any using (any?)
-open import Relation.Nullary using (Dec)
+open import Relation.Nullary.Decidable using (Dec)
 open DecSetoid DS renaming (Carrier to A)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Membership/Setoid.agda b/src/Data/Vec/Membership/Setoid.agda
index a03befdb39..68be682e7d 100644
--- a/src/Data/Vec/Membership/Setoid.agda
+++ b/src/Data/Vec/Membership/Setoid.agda
@@ -15,7 +15,7 @@ open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Unary.Any as Any
   using (Any; here; there; index)
 open import Data.Product using (∃; _×_; _,_)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Unary using (Pred)
 
 open Setoid S renaming (Carrier to A)
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 805570c42e..7f55bdc00c 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -27,9 +27,7 @@ open import Relation.Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; _≗_; refl; sym; trans; cong; cong₂; subst; module ≡-Reasoning)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary using (Dec; does; yes; no)
-open import Relation.Nullary.Decidable using (map′)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable using (Dec; does; yes; no; _×-dec_; map′)
 open import Relation.Nullary.Negation using (contradiction)
 
 open ≡-Reasoning
diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda
index 4a896b7aef..fdabddbf04 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Core.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda
@@ -17,15 +17,13 @@ open import Data.Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise; []; _∷_)
 open import Function.Base using (flip)
 open import Function.Bundles using (_⇔_; mk⇔)
+open import Level using (Level; _⊔_)
 open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; refl; cong)
-open import Relation.Nullary as Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Nullary.Sum using (_⊎-dec_)
+import Relation.Nullary as Nullary
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_; _⊎-dec_)
 open import Relation.Nullary.Negation
-open import Level using (Level; _⊔_)
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
index bac12f80c1..5f85d23894 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
@@ -18,9 +18,7 @@ open import Function.Base using (_∘_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
-open import Relation.Nullary
-open import Relation.Nullary.Decidable using (map′)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable using (yes; no; _×-dec_; map′)
 open import Relation.Unary using (Pred)
 
 private
diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda
index b16340ef6b..d59686bdad 100644
--- a/src/Data/Vec/Relation/Unary/All.agda
+++ b/src/Data/Vec/Relation/Unary/All.agda
@@ -17,9 +17,7 @@ open import Data.Vec.Membership.Propositional renaming (_∈_ to _∈ₚ_)
 import Data.Vec.Membership.Setoid as SetoidMembership
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no)
 open import Relation.Unary hiding (_∈_)
 open import Relation.Binary using (Setoid; _Respects_)
 open import Relation.Binary.PropositionalEquality as P using (subst)
diff --git a/src/Data/Vec/Relation/Unary/AllPairs.agda b/src/Data/Vec/Relation/Unary/AllPairs.agda
index adf5af2c9d..58e500a9f0 100644
--- a/src/Data/Vec/Relation/Unary/AllPairs.agda
+++ b/src/Data/Vec/Relation/Unary/AllPairs.agda
@@ -21,9 +21,7 @@ open import Relation.Binary as B using (Rel; _⇒_)
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
-open import Relation.Nullary using (yes; no)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable as Dec using (yes; no; _×-dec_)
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda
index a54991976f..f400e25f86 100644
--- a/src/Data/Vec/Relation/Unary/Any.agda
+++ b/src/Data/Vec/Relation/Unary/Any.agda
@@ -15,10 +15,8 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec.Base as Vec using (Vec; []; [_]; _∷_)
 open import Data.Product as Prod using (∃; _,_)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary using (¬_; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_)
 open import Relation.Unary
 
 private
diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda
index 9faa49d464..17040a4862 100644
--- a/src/Data/Vec/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda
@@ -26,7 +26,7 @@ open import Function.Base
 open import Function.Inverse using (_↔_; inverse)
   renaming (_∘_ to _∘↔_; id to id↔)
 open import Level using (Level)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Unary hiding (_∈_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_; refl)
diff --git a/src/Data/Vec/Relation/Unary/Linked.agda b/src/Data/Vec/Relation/Unary/Linked.agda
index 9183ac325d..641452fac1 100644
--- a/src/Data/Vec/Relation/Unary/Linked.agda
+++ b/src/Data/Vec/Relation/Unary/Linked.agda
@@ -18,9 +18,7 @@ open import Relation.Binary as B using (Rel; _⇒_)
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
-open import Relation.Nullary using (yes; no)
-open import Relation.Nullary.Decidable as Dec using (map′)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable as Dec using (yes; no; _×-dec_; map′)
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
index 3935a263c4..8fa3157bde 100644
--- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
@@ -22,7 +22,7 @@ open import Function.Base using (_∘_; flip; _on_)
 open import Relation.Binary using (Rel; Transitive; DecSetoid)
 open import Relation.Binary.PropositionalEquality using (_≢_)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary using (yes; no; does)
+open import Relation.Nullary.Decidable using (yes; no; does)
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
index acd1b916c8..e740fd8ad2 100644
--- a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
@@ -24,7 +24,7 @@ open import Relation.Binary using (Rel; Setoid)
 open import Relation.Binary.PropositionalEquality
   using (refl; _≡_; _≢_; sym; setoid)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Unary/Unique/Setoid.agda b/src/Data/Vec/Relation/Unary/Unique/Setoid.agda
index fae3073b9e..dd5cbb0c37 100644
--- a/src/Data/Vec/Relation/Unary/Unique/Setoid.agda
+++ b/src/Data/Vec/Relation/Unary/Unique/Setoid.agda
@@ -16,7 +16,7 @@ open import Data.Vec.Base
 import Data.Vec.Relation.Unary.AllPairs as AllPairsM
 open import Level using (_⊔_)
 open import Relation.Unary using (Pred)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 
 ------------------------------------------------------------------------
diff --git a/src/Data/W.agda b/src/Data/W.agda
index fc9464e8c9..81902e5a63 100644
--- a/src/Data/W.agda
+++ b/src/Data/W.agda
@@ -13,7 +13,7 @@ open import Function.Base using (_$_; _∘_; const)
 open import Data.Product using (_,_; -,_; proj₂)
 open import Data.Container.Core using (Container; ⟦_⟧; Shape; Position; _⇒_; ⟪_⟫)
 open import Data.Container.Relation.Unary.All using (□; all)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Agda.Builtin.Equality using (_≡_; refl)
 
 private
diff --git a/src/Data/W/Sized.agda b/src/Data/W/Sized.agda
index 655ab2911d..d977128900 100644
--- a/src/Data/W/Sized.agda
+++ b/src/Data/W/Sized.agda
@@ -14,7 +14,7 @@ open import Function.Base using (_$_; _∘_; const)
 open import Data.Product using (_,_; -,_; proj₂)
 open import Data.Container.Core as Container using (Container; ⟦_⟧; Shape; Position; _⇒_; ⟪_⟫)
 open import Data.Container.Relation.Unary.All using (□; all)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
 private
diff --git a/src/Function/Consequences.agda b/src/Function/Consequences.agda
index 0c98c0c2a1..e2c51e90d6 100644
--- a/src/Function/Consequences.agda
+++ b/src/Function/Consequences.agda
@@ -13,7 +13,7 @@ open import Function.Definitions
 open import Level
 open import Relation.Binary
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation.Core using (contraposition)
 
 private
diff --git a/src/Function/Metric/Definitions.agda b/src/Function/Metric/Definitions.agda
index e95e7b26a0..adf343aebb 100644
--- a/src/Function/Metric/Definitions.agda
+++ b/src/Function/Metric/Definitions.agda
@@ -15,7 +15,7 @@ open import Data.Product using (∃)
 open import Function.Metric.Core using (DistanceFunction)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 private
   variable
diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda
index 809533981f..bc7b6ba034 100644
--- a/src/Reflection/AST/Abstraction.agda
+++ b/src/Reflection/AST/Abstraction.agda
@@ -12,9 +12,7 @@ open import Data.List.Base as List using (List)
 open import Data.Product using (_×_; _,_; uncurry; <_,_>)
 open import Data.String as String using (String)
 open import Level
-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; _×-dec_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 
diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda
index 39a1b20ffa..0374f15102 100644
--- a/src/Reflection/AST/Argument.agda
+++ b/src/Reflection/AST/Argument.agda
@@ -11,17 +11,16 @@ module Reflection.AST.Argument where
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.Product using (_×_; _,_; uncurry; <_,_>)
 open import Data.Nat using (ℕ)
+open import Relation.Nullary.Decidable as Dec using (Dec; _×-dec_)
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality
+open import Level
+
 open import Reflection.AST.Argument.Visibility
 open import Reflection.AST.Argument.Relevance
 open import Reflection.AST.Argument.Quantity
 open import Reflection.AST.Argument.Modality
 open import Reflection.AST.Argument.Information as Information
-open import Relation.Nullary
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality
-open import Level
 
 private
   variable
diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda
index 0ba3f53bea..084ea24ea9 100644
--- a/src/Reflection/AST/Argument/Information.agda
+++ b/src/Reflection/AST/Argument/Information.agda
@@ -8,9 +8,9 @@
 
 module Reflection.AST.Argument.Information where
 
-open import Data.Product
+open import Data.Product.Base
 import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable using (_×-dec_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 
diff --git a/src/Reflection/AST/Argument/Modality.agda b/src/Reflection/AST/Argument/Modality.agda
index ca8d9519f7..4fc97dbd99 100644
--- a/src/Reflection/AST/Argument/Modality.agda
+++ b/src/Reflection/AST/Argument/Modality.agda
@@ -8,10 +8,9 @@
 
 module Reflection.AST.Argument.Modality where
 
-open import Data.Product
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Binary
+open import Data.Product.Base
+open import Relation.Nullary.Decidable as Dec using (_×-dec_)
+open import Relation.Binary using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
 
 open import Reflection.AST.Argument.Relevance as Relevance using (Relevance)
diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 2825b5c474..65e71f368c 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -16,8 +16,7 @@ open import Data.Product using (_×_; <_,_>; uncurry)
 open import Data.String as String using (String; _<+>_; intersperse; braces)
 open import Function.Base using (_∘′_)
 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)
 open import Relation.Binary using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
 
diff --git a/src/Reflection/AST/Show.agda b/src/Reflection/AST/Show.agda
index 8c14238669..66341ae7ed 100644
--- a/src/Reflection/AST/Show.agda
+++ b/src/Reflection/AST/Show.agda
@@ -19,7 +19,7 @@ import Data.Nat.Show as ℕ
 open import Data.Product using (_×_; _,_)
 open import Data.String as String
 import Data.Word as Word
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Function.Base using (id; _∘′_; case_of_)
 
 open import Reflection.AST.Abstraction hiding (map)
diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda
index ddb02b4afe..19b38f10e7 100644
--- a/src/Reflection/AST/Term.agda
+++ b/src/Reflection/AST/Term.agda
@@ -16,9 +16,7 @@ import Data.Product.Properties as Product
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.String as String using (String)
 open import Function.Base using (_∘_)
-open import Relation.Nullary
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 
@@ -168,7 +166,7 @@ arg i a ≟-ArgType arg i′ a′ = unArg-dec (a ≟ a′)
 _≟-Telescope_ : DecidableEquality Telescope
 [] ≟-Telescope [] = yes refl
 ((x , t) ∷ tel) ≟-Telescope ((x′ , t′) ∷ tel′) = Lₚ.∷-dec
-  (map′ (uncurry (cong₂ _,_)) Product.,-injective ((x String.≟ x′) ×-dec (t ≟-ArgTerm t′)))
+  (Dec.map′ (uncurry (cong₂ _,_)) Product.,-injective ((x String.≟ x′) ×-dec (t ≟-ArgTerm t′)))
   (tel ≟-Telescope tel′)
 [] ≟-Telescope (_ ∷ _) = no λ ()
 (_ ∷ _) ≟-Telescope [] = no λ ()
diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
index 4c4cd9b8e3..2c8b94082c 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/src/Relation/Binary/Bundles.agda
@@ -11,7 +11,7 @@
 module Relation.Binary.Bundles where
 
 open import Level
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.Core
 open import Relation.Binary.Definitions
 open import Relation.Binary.Structures
diff --git a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
index e251196768..893e9126a4 100644
--- a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
+++ b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
@@ -8,7 +8,7 @@
 
 module Relation.Binary.Construct.Closure.Reflexive.Properties where
 
-open import Data.Product as Prod
+open import Data.Product.Base as Prod
 open import Data.Sum.Base as Sum
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Function.Base using (id)
@@ -18,8 +18,6 @@ open import Relation.Binary.Construct.Closure.Reflexive
 open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Sum using (_⊎-dec_)
 open import Relation.Unary using (Pred)
 
 private
diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda
index b65dbb0414..6f378a6ff1 100644
--- a/src/Relation/Binary/Construct/Intersection.agda
+++ b/src/Relation/Binary/Construct/Intersection.agda
@@ -8,13 +8,12 @@
 
 module Relation.Binary.Construct.Intersection where
 
-open import Data.Product
+open import Data.Product.Base
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary
-open import Relation.Nullary using (yes; no)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable using (yes; no; _×-dec_)
 
 private
   variable
diff --git a/src/Relation/Binary/Construct/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda
index c36a314d99..aa51ef60b9 100644
--- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda
+++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda
@@ -11,7 +11,7 @@ open import Algebra.Core
 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 (¬_)
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 open import Relation.Binary.Lattice using (Infimum)
 
diff --git a/src/Relation/Binary/Construct/NaturalOrder/Right.agda b/src/Relation/Binary/Construct/NaturalOrder/Right.agda
index b3ee31e03f..ad4c78f9ea 100644
--- a/src/Relation/Binary/Construct/NaturalOrder/Right.agda
+++ b/src/Relation/Binary/Construct/NaturalOrder/Right.agda
@@ -11,7 +11,7 @@ open import Algebra.Core using (Op₂)
 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 (¬_)
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
 module Relation.Binary.Construct.NaturalOrder.Right
diff --git a/src/Relation/Binary/Construct/NonStrictToStrict.agda b/src/Relation/Binary/Construct/NonStrictToStrict.agda
index 8f1099b4a9..eed860f088 100644
--- a/src/Relation/Binary/Construct/NonStrictToStrict.agda
+++ b/src/Relation/Binary/Construct/NonStrictToStrict.agda
@@ -11,13 +11,12 @@ open import Relation.Binary
 module Relation.Binary.Construct.NonStrictToStrict
   {a ℓ₁ ℓ₂} {A : Set a} (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) where
 
-open import Data.Product using (_×_; _,_; proj₁; proj₂)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_∘_; flip)
 open import Relation.Nullary using (¬_; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (¬?)
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Decidable using (¬?; _×-dec_)
 
 private
   _≉_ : Rel A ℓ₁
diff --git a/src/Relation/Binary/Construct/StrictToNonStrict.agda b/src/Relation/Binary/Construct/StrictToNonStrict.agda
index 05c2b65810..dd1b7980ce 100644
--- a/src/Relation/Binary/Construct/StrictToNonStrict.agda
+++ b/src/Relation/Binary/Construct/StrictToNonStrict.agda
@@ -17,13 +17,12 @@ module Relation.Binary.Construct.StrictToNonStrict
   (_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂)
   where
 
-open import Data.Product
+open import Data.Product.Base
 open import Data.Sum.Base
 open import Data.Empty
 open import Function.Base
 open import Relation.Binary.Consequences
-open import Relation.Nullary
-open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Decidable using (_⊎-dec_; yes; no)
 
 ------------------------------------------------------------------------
 -- Conversion
diff --git a/src/Relation/Binary/Construct/Union.agda b/src/Relation/Binary/Construct/Union.agda
index f4975601f6..b98d7dfb98 100644
--- a/src/Relation/Binary/Construct/Union.agda
+++ b/src/Relation/Binary/Construct/Union.agda
@@ -8,13 +8,12 @@
 
 module Relation.Binary.Construct.Union where
 
-open import Data.Product
+open import Data.Product.Base
 open import Data.Sum.Base as Sum
 open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary
-open import Relation.Nullary using (yes; no)
-open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_)
 
 private
   variable
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
index 80f4d74bb6..3618d3dea3 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
@@ -16,7 +16,7 @@ open import Function.Base using (_⟨_⟩_)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary as B using (_⇒_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.Indexed.Homogeneous.Core
 open import Relation.Binary.Indexed.Homogeneous.Structures
 
diff --git a/src/Relation/Binary/Morphism/RelMonomorphism.agda b/src/Relation/Binary/Morphism/RelMonomorphism.agda
index 1b27014052..5da0d18524 100644
--- a/src/Relation/Binary/Morphism/RelMonomorphism.agda
+++ b/src/Relation/Binary/Morphism/RelMonomorphism.agda
@@ -20,7 +20,7 @@ module Relation.Binary.Morphism.RelMonomorphism
   where
 
 open import Data.Sum.Base as Sum
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable
 
 open IsRelMonomorphism isMonomorphism
diff --git a/src/Relation/Binary/Properties/ApartnessRelation.agda b/src/Relation/Binary/Properties/ApartnessRelation.agda
index 1a7f392d36..c043135852 100644
--- a/src/Relation/Binary/Properties/ApartnessRelation.agda
+++ b/src/Relation/Binary/Properties/ApartnessRelation.agda
@@ -18,7 +18,7 @@ open import Function.Base using (_∘₂_)
 open import Relation.Binary.Definitions using (Reflexive)
 open import Relation.Binary.Consequences using (sym⇒¬-sym; cotrans⇒¬-trans)
 open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 ¬#-isEquivalence : Reflexive _≈_ → IsApartnessRelation _≈_ _#_ →
                    IsEquivalence (¬_ ∘₂ _#_)
diff --git a/src/Relation/Binary/Properties/DecTotalOrder.agda b/src/Relation/Binary/Properties/DecTotalOrder.agda
index 289aae812e..c3589b01ad 100644
--- a/src/Relation/Binary/Properties/DecTotalOrder.agda
+++ b/src/Relation/Binary/Properties/DecTotalOrder.agda
@@ -16,7 +16,7 @@ open DecTotalOrder DT hiding (trans)
 import Relation.Binary.Construct.Converse as Converse
 import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
 import Relation.Binary.Properties.TotalOrder totalOrder as TotalOrderProperties
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 ------------------------------------------------------------------------
 -- _≥_ - the flipped relation is also a total order
diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda
index 66aa8694cd..74174d6de1 100644
--- a/src/Relation/Binary/Properties/Setoid.agda
+++ b/src/Relation/Binary/Properties/Setoid.agda
@@ -8,7 +8,7 @@
 
 open import Data.Product using (_,_)
 open import Function.Base using (_∘_; id; _$_; flip)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary
 
diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda
index b2bdb66e31..dc18df5dd1 100644
--- a/src/Relation/Binary/Properties/TotalOrder.agda
+++ b/src/Relation/Binary/Properties/TotalOrder.agda
@@ -19,7 +19,7 @@ import Relation.Binary.Construct.Converse as Converse
 import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
 import Relation.Binary.Properties.Poset poset as PosetProperties
 open import Relation.Binary.Consequences
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (contradiction)
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index 12a79f13ed..4c7e71b2cd 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -15,7 +15,7 @@ open import Function.Equality using (Π; _⟶_; ≡-setoid)
 open import Level using (Level; _⊔_)
 open import Data.Product using (∃)
 
-open import Relation.Nullary using (yes ; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable
 open import Relation.Binary
 open import Relation.Binary.Indexed.Heterogeneous
diff --git a/src/Relation/Binary/Reasoning/Base/Double.agda b/src/Relation/Binary/Reasoning/Base/Double.agda
index f30636ba64..1b092c2c5f 100644
--- a/src/Relation/Binary/Reasoning/Base/Double.agda
+++ b/src/Relation/Binary/Reasoning/Base/Double.agda
@@ -21,7 +21,7 @@ open import Level using (Level; _⊔_; Lift; lift)
 open import Function.Base using (case_of_; id)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym)
-open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Nullary.Decidable using (Dec; yes; no)
 open import Relation.Nullary.Decidable using (True; toWitness)
 
 open IsPreorder isPreorder
diff --git a/src/Relation/Binary/Reasoning/Base/Partial.agda b/src/Relation/Binary/Reasoning/Base/Partial.agda
index dd60628c4c..46d5a27ba0 100644
--- a/src/Relation/Binary/Reasoning/Base/Partial.agda
+++ b/src/Relation/Binary/Reasoning/Base/Partial.agda
@@ -11,7 +11,7 @@ open import Relation.Binary.Definitions
 open import Level using (_⊔_)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_)
-open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Nullary.Decidable using (Dec; yes; no)
 open import Relation.Nullary.Decidable using (True)
 
 module Relation.Binary.Reasoning.Base.Partial
diff --git a/src/Relation/Binary/Reasoning/Base/Triple.agda b/src/Relation/Binary/Reasoning/Base/Triple.agda
index 32c384d24c..b44f61226e 100644
--- a/src/Relation/Binary/Reasoning/Base/Triple.agda
+++ b/src/Relation/Binary/Reasoning/Base/Triple.agda
@@ -24,7 +24,7 @@ open import Function.Base using (case_of_; id)
 open import Level using (Level; _⊔_; Lift; lift)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym)
-open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Nullary.Decidable using (Dec; yes; no)
 open import Relation.Nullary.Decidable using (True; toWitness)
 
 open IsPreorder isPreorder
diff --git a/src/Relation/Nary.agda b/src/Relation/Nary.agda
index d5c38df741..107e3772f6 100644
--- a/src/Relation/Nary.agda
+++ b/src/Relation/Nary.agda
@@ -24,9 +24,8 @@ open import Data.Product.Nary.NonDependent
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_$_; _∘′_)
 open import Function.Nary.NonDependent
-open import Relation.Nullary using (¬_; Dec; yes; no; _because_)
-import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _because_; _×-dec_)
 import Relation.Unary as Unary
 open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst)
 
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index b4766227c6..4eb7cb0b20 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -15,9 +15,20 @@ open import Agda.Builtin.Equality
 ------------------------------------------------------------------------
 -- Re-exports
 
-open import Relation.Nullary.Negation.Core public using (¬_)
-open import Relation.Nullary.Reflects public using (Reflects; ofʸ; ofⁿ)
-open import Relation.Nullary.Decidable.Core public using (Dec; yes; no; does; proof; recompute; _because_)
+open import Relation.Nullary.Negation.Core public using
+  ( ¬_; _¬-⊎_
+  ; contradiction; contradiction₂; contraposition
+  )
+
+open import Relation.Nullary.Reflects public using
+  ( Reflects; ofʸ; ofⁿ
+  ; _×-reflects_; _⊎-reflects_; _→-reflects_
+  )
+
+open import Relation.Nullary.Decidable.Core public using
+  ( Dec; does; proof; yes; no; _because_; recompute
+  ; ¬?; _×-dec_; _⊎-dec_; _→-dec_
+  )
 
 ------------------------------------------------------------------------
 -- Irrelevant types
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index 1dc26b171e..48724feb7f 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -12,11 +12,12 @@
 module Relation.Nullary.Decidable.Core where
 
 open import Level using (Level; Lift)
-open import Data.Bool.Base using (Bool; false; true; not; T)
+open import Data.Bool.Base using (Bool; false; true; not; T; _∧_; _∨_)
 open import Data.Unit.Base using (⊤)
 open import Data.Empty using (⊥)
 open import Data.Empty.Irrelevant using (⊥-elim)
-open import Data.Product
+open import Data.Product using (_×_)
+open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
 open import Relation.Nullary.Reflects
 open import Relation.Nullary.Negation.Core
@@ -63,10 +64,25 @@ recompute (no ¬p) x = ⊥-elim (¬p x)
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
 
+infixr 1 _⊎-dec_
+infixr 2 _×-dec_ _→-dec_
+
 ¬? : Dec P → Dec (¬ P)
 does  (¬? p?) = not (does p?)
 proof (¬? p?) = ¬-reflects (proof p?)
 
+_×-dec_ : Dec P → Dec Q → Dec (P × Q)
+does  (p? ×-dec q?) = does p? ∧ does q?
+proof (p? ×-dec q?) = proof p? ×-reflects proof q?
+
+_⊎-dec_ : Dec P → Dec Q → Dec (P ⊎ Q)
+does  (p? ⊎-dec q?) = does p? ∨ does q?
+proof (p? ⊎-dec q?) = proof p? ⊎-reflects proof q?
+
+_→-dec_ : Dec P → Dec Q → Dec (P → Q)
+does  (p? →-dec q?) = not (does p?) ∨ does q?
+proof (p? →-dec q?) = proof p? →-reflects proof q?
+
 ------------------------------------------------------------------------
 -- Relationship with booleans
 
diff --git a/src/Relation/Nullary/Implication.agda b/src/Relation/Nullary/Implication.agda
index cdf257c78d..90ff3514e1 100644
--- a/src/Relation/Nullary/Implication.agda
+++ b/src/Relation/Nullary/Implication.agda
@@ -1,36 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Implications of nullary relations
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Relation.Nullary.Implication where
 
-open import Data.Bool.Base
-open import Data.Empty
-open import Function.Base
-open import Relation.Nullary
-open import Level
+{-# WARNING_ON_IMPORT
+"Relation.Nullary.Implication was deprecated in v2.0.
+Use `Relation.Nullary.Decidable` or `Relation.Nullary` instead."
+#-}
 
-private
-  variable
-    p q : Level
-    P : Set p
-    Q : Set q
-
-------------------------------------------------------------------------
--- Some properties which are preserved by _→_.
-
-infixr 2 _→-reflects_ _→-dec_
-
-_→-reflects_ : ∀ {bp bq} → Reflects P bp → Reflects Q bq →
-                           Reflects (P → Q) (not bp ∨ bq)
-ofʸ  p →-reflects ofʸ  q = ofʸ (const q)
-ofʸ  p →-reflects ofⁿ ¬q = ofⁿ (¬q ∘ (_$ p))
-ofⁿ ¬p →-reflects _      = ofʸ (⊥-elim ∘ ¬p)
-
-_→-dec_ : Dec P → Dec Q → Dec (P → Q)
-does  (p? →-dec q?) = not (does p?) ∨ does q?
-proof (p? →-dec q?) = proof p? →-reflects proof q?
+open import Relation.Nullary.Decidable.Core public using (_→-dec_)
+open import Relation.Nullary.Reflects public using (_→-reflects_)
diff --git a/src/Relation/Nullary/Negation/Core.agda b/src/Relation/Nullary/Negation/Core.agda
index 3a245b79a9..520914def3 100644
--- a/src/Relation/Nullary/Negation/Core.agda
+++ b/src/Relation/Nullary/Negation/Core.agda
@@ -9,10 +9,10 @@
 module Relation.Nullary.Negation.Core where
 
 open import Data.Bool.Base using (not)
-open import Data.Empty hiding (⊥-elim)
-open import Data.Empty.Irrelevant
-open import Data.Product.Base
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Empty using (⊥)
+open import Data.Empty.Irrelevant using (⊥-elim)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Sum.Base using (_⊎_; [_,_]; inj₁; inj₂)
 open import Function.Base using (flip; _$_; _∘_; const)
 open import Level
 
@@ -39,6 +39,13 @@ DoubleNegation P = ¬ ¬ P
 Stable : Set p → Set p
 Stable P = ¬ ¬ P → P
 
+------------------------------------------------------------------------
+-- Relationship to product and sum
+
+infixr 1 _¬-⊎_
+_¬-⊎_ : ¬ P → ¬ Q → ¬ (P ⊎ Q)
+_¬-⊎_ = [_,_]
+
 ------------------------------------------------------------------------
 -- Uses of negation
 
diff --git a/src/Relation/Nullary/Product.agda b/src/Relation/Nullary/Product.agda
index 8bdfc01588..0d87c30fcc 100644
--- a/src/Relation/Nullary/Product.agda
+++ b/src/Relation/Nullary/Product.agda
@@ -1,37 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Products of nullary relations
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Relation.Nullary.Product where
 
-open import Data.Bool.Base
-open import Data.Product
-open import Function.Base using (_∘_)
-open import Level
-open import Relation.Nullary.Reflects
-open import Relation.Nullary
+{-# WARNING_ON_IMPORT
+"Relation.Nullary.Product was deprecated in v2.0.
+Use `Relation.Nullary.Decidable` or `Relation.Nullary` instead."
+#-}
 
-private
-  variable
-    p q : Level
-    P : Set p
-    Q : Set q
-
-------------------------------------------------------------------------
--- Some properties which are preserved by _×_.
-
-infixr 2 _×-reflects_ _×-dec_
-
-_×-reflects_ : ∀ {bp bq} → Reflects P bp → Reflects Q bq →
-                           Reflects (P × Q) (bp ∧ bq)
-ofʸ  p ×-reflects ofʸ  q = ofʸ (p , q)
-ofʸ  p ×-reflects ofⁿ ¬q = ofⁿ (¬q ∘ proj₂)
-ofⁿ ¬p ×-reflects _      = ofⁿ (¬p ∘ proj₁)
-
-_×-dec_ : Dec P → Dec Q → Dec (P × Q)
-does  (p? ×-dec q?) = does p? ∧ does q?
-proof (p? ×-dec q?) = proof p? ×-reflects proof q?
+open import Relation.Nullary.Decidable.Core public using (_×-dec_)
+open import Relation.Nullary.Reflects public using (_×-reflects_)
diff --git a/src/Relation/Nullary/Reflects.agda b/src/Relation/Nullary/Reflects.agda
index 683d9924c6..c6fcaf6ea6 100644
--- a/src/Relation/Nullary/Reflects.agda
+++ b/src/Relation/Nullary/Reflects.agda
@@ -9,17 +9,20 @@
 module Relation.Nullary.Reflects where
 
 open import Agda.Builtin.Equality
+
 open import Data.Bool.Base
 open import Data.Empty
-open import Level
-open import Function.Base using (_$_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Level using (Level)
+open import Function.Base using (_$_; _∘_; const)
 
 open import Relation.Nullary.Negation.Core
 
 private
   variable
-    p : Level
-    P : Set p
+    p q : Level
+    P Q : Set p
 
 ------------------------------------------------------------------------
 -- `Reflects` idiom.
@@ -48,16 +51,37 @@ invert : ∀ {b} → Reflects P b → if b then P else ¬ P
 invert (ofʸ  p) = p
 invert (ofⁿ ¬p) = ¬p
 
-
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.
 
 -- If we can decide P, then we can decide its negation.
-
 ¬-reflects : ∀ {b} → Reflects P b → Reflects (¬ P) (not b)
 ¬-reflects (ofʸ  p) = ofⁿ (_$ p)
 ¬-reflects (ofⁿ ¬p) = ofʸ ¬p
 
+-- If we can decide P and Q then we can decide their product
+infixr 2 _×-reflects_
+_×-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b →
+               Reflects (P × Q) (a ∧ b)
+ofʸ  p ×-reflects ofʸ  q = ofʸ (p , q)
+ofʸ  p ×-reflects ofⁿ ¬q = ofⁿ (¬q ∘ proj₂)
+ofⁿ ¬p ×-reflects _      = ofⁿ (¬p ∘ proj₁)
+
+
+infixr 1 _⊎-reflects_
+_⊎-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b →
+               Reflects (P ⊎ Q) (a ∨ b)
+ofʸ  p ⊎-reflects      _ = ofʸ (inj₁ p)
+ofⁿ ¬p ⊎-reflects ofʸ  q = ofʸ (inj₂ q)
+ofⁿ ¬p ⊎-reflects ofⁿ ¬q = ofⁿ (¬p ¬-⊎ ¬q)
+
+infixr 2 _→-reflects_
+_→-reflects_ : ∀ {a b} → Reflects P a → Reflects Q b →
+                Reflects (P → Q) (not a ∨ b)
+ofʸ  p →-reflects ofʸ  q = ofʸ (const q)
+ofʸ  p →-reflects ofⁿ ¬q = ofⁿ (¬q ∘ (_$ p))
+ofⁿ ¬p →-reflects _      = ofʸ (⊥-elim ∘ ¬p)
+
 ------------------------------------------------------------------------
 -- Other lemmas
 
diff --git a/src/Relation/Nullary/Sum.agda b/src/Relation/Nullary/Sum.agda
index 2c025fe47f..b46fbf9545 100644
--- a/src/Relation/Nullary/Sum.agda
+++ b/src/Relation/Nullary/Sum.agda
@@ -1,40 +1,18 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Sums of nullary relations
+-- This module is DEPRECATED.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
 module Relation.Nullary.Sum where
 
-open import Data.Bool.Base
-open import Data.Sum.Base
-open import Data.Empty
-open import Level
-open import Relation.Nullary.Reflects
-open import Relation.Nullary
+{-# WARNING_ON_IMPORT
+"Relation.Nullary.Sum was deprecated in v2.0.
+Use `Relation.Nullary.Decidable` or `Relation.Nullary` instead."
+#-}
 
-private
-  variable
-    p q : Level
-    P : Set p
-    Q : Set q
-
-------------------------------------------------------------------------
--- Some properties which are preserved by _⊎_.
-
-infixr 1 _¬-⊎_ _⊎-reflects_ _⊎-dec_
-
-_¬-⊎_ : ¬ P → ¬ Q → ¬ (P ⊎ Q)
-_¬-⊎_ = [_,_]
-
-_⊎-reflects_ : ∀ {bp bq} → Reflects P bp → Reflects Q bq →
-                           Reflects (P ⊎ Q) (bp ∨ bq)
-ofʸ  p ⊎-reflects      _ = ofʸ (inj₁ p)
-ofⁿ ¬p ⊎-reflects ofʸ  q = ofʸ (inj₂ q)
-ofⁿ ¬p ⊎-reflects ofⁿ ¬q = ofⁿ (¬p ¬-⊎ ¬q)
-
-_⊎-dec_ : Dec P → Dec Q → Dec (P ⊎ Q)
-does  (p? ⊎-dec q?) = does p? ∨ does q?
-proof (p? ⊎-dec q?) = proof p? ⊎-reflects proof q?
+open import Relation.Nullary.Negation.Core public using (_¬-⊎_)
+open import Relation.Nullary.Reflects public using (_⊎-reflects_)
+open import Relation.Nullary.Decidable.Core public using (_⊎-dec_)
diff --git a/src/Relation/Unary/Indexed.agda b/src/Relation/Unary/Indexed.agda
index 8ce3622ce3..49e36d3679 100644
--- a/src/Relation/Unary/Indexed.agda
+++ b/src/Relation/Unary/Indexed.agda
@@ -10,7 +10,7 @@ module Relation.Unary.Indexed  where
 
 open import Data.Product using (∃; _×_)
 open import Level
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 
 IPred : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
 IPred A ℓ = ∀ {i} → A i → Set ℓ
diff --git a/src/Relation/Unary/Polymorphic/Properties.agda b/src/Relation/Unary/Polymorphic/Properties.agda
index e40a29c361..61b25678b9 100644
--- a/src/Relation/Unary/Polymorphic/Properties.agda
+++ b/src/Relation/Unary/Polymorphic/Properties.agda
@@ -11,7 +11,7 @@ module Relation.Unary.Polymorphic.Properties where
 
 open import Level using (Level)
 open import Relation.Binary.Definitions hiding (Decidable; Universal)
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Unary hiding (∅; U)
 open import Relation.Unary.Polymorphic
 open import Data.Unit.Polymorphic.Base using (tt)
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index 08a258b803..0dc39837b3 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -16,10 +16,7 @@ open import Relation.Binary.Core as Binary
 open import Relation.Binary.Definitions hiding (Decidable; Universal; Irrelevant)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 open import Relation.Unary
-open import Relation.Nullary using (yes; no)
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Nullary.Sum using (_⊎-dec_)
-open import Relation.Nullary.Decidable using (¬?)
+open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?)
 open import Function.Base using (id; _$_; _∘_)
 
 private
diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda
index ffa98b22d6..16e03a95df 100644
--- a/src/Test/Golden.agda
+++ b/src/Test/Golden.agda
@@ -96,7 +96,7 @@ open import Data.Unit.Base using (⊤)
 
 open import Function.Base using (id; _$_; case_of_)
 
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 
 open import Codata.Musical.Notation using (♯_)
 open import IO
diff --git a/src/Text/Pretty/Core.agda b/src/Text/Pretty/Core.agda
index e09d9e66b5..f546bc5962 100644
--- a/src/Text/Pretty/Core.agda
+++ b/src/Text/Pretty/Core.agda
@@ -33,7 +33,7 @@ open import Data.String.Base as String
   using (String; length; replicate; _++_; unlines)
 open import Data.String.Unsafe as Stringₚ
 open import Function.Base
-open import Relation.Nullary using (Dec)
+open import Relation.Nullary.Decidable using (Dec)
 open import Relation.Unary using (IUniversal; _⇒_; U)
 open import Relation.Binary.PropositionalEquality
 
diff --git a/src/Text/Regex/Base.agda b/src/Text/Regex/Base.agda
index d2d1003318..adfde3e03d 100644
--- a/src/Text/Regex/Base.agda
+++ b/src/Text/Regex/Base.agda
@@ -18,7 +18,7 @@ open import Data.List.Relation.Unary.Any using (Any)
 open import Data.List.Relation.Unary.All using (All)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Unary using (Pred)
 open import Relation.Binary.PropositionalEquality
diff --git a/src/Text/Regex/Derivative/Brzozowski.agda b/src/Text/Regex/Derivative/Brzozowski.agda
index e1aa7bdcc0..57dd1f165d 100644
--- a/src/Text/Regex/Derivative/Brzozowski.agda
+++ b/src/Text/Regex/Derivative/Brzozowski.agda
@@ -15,7 +15,7 @@ open import Data.List.Relation.Binary.Equality.Propositional
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
 
 open import Function.Base using (_$_; _∘′_; case_of_)
-open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Nullary.Decidable using (Dec; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Nullary.Decidable using (map′; ¬?)
 open import Relation.Binary using (Decidable)
diff --git a/src/Text/Regex/Properties.agda b/src/Text/Regex/Properties.agda
index bc22aa5c4d..b198972e64 100644
--- a/src/Text/Regex/Properties.agda
+++ b/src/Text/Regex/Properties.agda
@@ -13,15 +13,14 @@ module Text.Regex.Properties {a e r} (P? : DecPoset a e r) where
 open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Relation.Unary.All using (all?)
 open import Data.List.Relation.Unary.Any using (any?)
-open import Data.Product using (_×_; _,_; uncurry)
+open import Data.Product.Base using (_×_; _,_; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_$_)
 
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Nullary.Decidable using (map′; ¬?)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Decidable
+  using (Dec; yes; no; map′; ¬?; _×-dec_; _⊎-dec_)
+open import Relation.Nullary.Negation
+  using (¬_; contradiction)
 
 import Relation.Unary  as U
 open import Relation.Binary using (Decidable)
diff --git a/src/Text/Regex/SmartConstructors.agda b/src/Text/Regex/SmartConstructors.agda
index a9f2fb2a14..e27ae2a1d3 100644
--- a/src/Text/Regex/SmartConstructors.agda
+++ b/src/Text/Regex/SmartConstructors.agda
@@ -17,7 +17,7 @@ open import Data.List.Base using ([])
 open import Data.List.Relation.Ternary.Appending.Propositional
 open import Data.Sum.Base using (inj₁; inj₂; fromInj₁; fromInj₂)
 
-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.Binary.PropositionalEquality using (refl)
 
diff --git a/tests/reflection/assumption/Main.agda b/tests/reflection/assumption/Main.agda
index 5146743bde..d7f30d3118 100644
--- a/tests/reflection/assumption/Main.agda
+++ b/tests/reflection/assumption/Main.agda
@@ -16,7 +16,7 @@ open import Reflection.AST.Literal hiding (_≟_)
 open import Reflection.AST.Argument using (Arg; unArg; arg)
 open import Reflection.AST.DeBruijn
 open import Reflection.AST.Show
-open import Relation.Nullary using (does)
+open import Relation.Nullary.Decidable using (does)
 
 open import Effect.Monad
 open RawMonad {{...}}