Stage 2 of refactoring of Relation.Nullary (#1869)

* Deprecate Relation.Nullary.(Sum/Product/Implication)

* Some grepped refining of imports

* Added missing deprecation warnings

Author: MatthewDaggitt

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`.

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:

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

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

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

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
 
 

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

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}

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

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