[Refactor] imports to use Relation.Nullary.Irrelevant (#2676)

* New file Irrelevant

* Module Irrelevant description

* add Irrelevant file in CHANGELOG

* remove blank line

* Update src/Relation/Nullary/Irrelevant.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

* Fix

* Update CHANGELOG.md

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

---------

Co-authored-by: Jacques Carette <carette@mcmaster.ca>
Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

Author: 3 people

CHANGELOG.md

@@ -28,6 +28,9 @@ Non-backwards compatible changes
 Minor improvements
 ------------------
 
+* Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary`
+  to its own dedicated module `Relation.Nullary.Irrelevant`.
+
 Deprecated modules
 ------------------
 

src/Data/List/Fresh/Membership/Setoid/Properties.agda

@@ -26,7 +26,7 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; fromInj₂)
 open import Function.Base using (id; _∘′_; _$_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Negation.Core using (¬_)
-open import Relation.Nullary using (Irrelevant)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Unary as Unary using (Pred)
 import Relation.Binary.Definitions as Binary using (_Respectsˡ_; Irrelevant)
 import Relation.Binary.PropositionalEquality.Core as ≡

src/Data/List/Relation/Binary/Pointwise.agda

@@ -18,19 +18,24 @@ open import Data.List.Properties using (≡-dec; length-++)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
-open import Data.Fin.Base using (Fin; toℕ; cast) renaming (zero to fzero; suc to fsuc)
+open import Data.Fin.Base
+  using (Fin; toℕ; cast)
+  renaming (zero to fzero; suc to fsuc)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Nat.Properties
-open import Level
-open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec using (map′)
-open import Relation.Unary as U using (Pred)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Core renaming (Rel to Rel₂)
-open import Relation.Binary.Definitions using (Reflexive; _Respects_; _Respects₂_)
+open import Relation.Binary.Definitions
+  using (Reflexive; _Respects_; _Respects₂_)
 open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset)
-open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder)
+open import Relation.Binary.Structures
+  using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
+open import Relation.Nullary.Decidable as Dec
+  using (map′; yes; no; Dec; _because_)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Unary as U using (Pred)
 
 private
   variable

src/Data/List/Relation/Unary/All.agda

@@ -19,8 +19,8 @@ open import Effect.Applicative
 open import Effect.Monad
 open import Function.Base using (_∘_; _∘′_; id; const)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable.Core as Dec
+  using (_×-dec_; yes; no; map′)
 open import Relation.Unary hiding (_∈_)
 import Relation.Unary.Properties as Unary
 open import Relation.Binary.Bundles using (Setoid)

src/Data/Maybe/Relation/Unary/Any.agda

@@ -16,8 +16,7 @@ open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 open import Relation.Unary
   using (Pred; _⊆_; _∩_; Decidable; Irrelevant; Satisfiable)
-open import Relation.Nullary hiding (Irrelevant)
-import Relation.Nullary.Decidable as Dec using (Dec; yes; no; map)
+open import Relation.Nullary.Decidable as Dec using (Dec; yes; no)
 
 ------------------------------------------------------------------------
 -- Definition

src/Data/Nat/Properties.agda

@@ -44,11 +44,11 @@ open import Relation.Binary.Core
 open import Relation.Binary
 open import Relation.Binary.Consequences using (flip-Connex; wlog)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Decidable
-  using (True; via-injection; map′; recompute)
+  using (True; via-injection; map′; recompute; no; yes; Dec; _because_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
-open import Relation.Nullary.Reflects using (fromEquivalence)
+open import Relation.Nullary.Reflects
+  using (fromEquivalence; Reflects; invert)
 
 open import Algebra.Definitions {A = ℕ} _≡_
   hiding (LeftCancellative; RightCancellative; Cancellative)

src/Data/Unit/Properties.agda

@@ -11,7 +11,6 @@ module Data.Unit.Properties where
 open import Data.Sum.Base using (inj₁)
 open import Data.Unit.Base using (⊤)
 open import Level using (0ℓ)
-open import Relation.Nullary using (Irrelevant; yes)
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Poset; DecTotalOrder)
 open import Relation.Binary.Structures
@@ -22,6 +21,9 @@ open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; trans)
 open import Relation.Binary.PropositionalEquality.Properties
   using (setoid; decSetoid; isEquivalence)
+open import Relation.Nullary.Decidable.Core using (yes)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
+
 
 ------------------------------------------------------------------------
 -- Irrelevancy

src/Data/Vec/Relation/Binary/Lex/NonStrict.agda

@@ -33,7 +33,7 @@ open import Relation.Binary.Definitions
   using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric; Trans
         ; Decidable; Total; Trichotomous)
 import Relation.Binary.Construct.NonStrictToStrict as Conv
-open import Relation.Nullary hiding (Irrelevant)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 
 private
   variable

src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda

@@ -28,8 +28,8 @@ open import Relation.Binary.Structures
         ; IsDecTotalOrder)
 open import Relation.Binary.Definitions
   using (Minimum; Transitive; Total; Decidable; Irrelevant; Antisymmetric)
-open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Infimum using (⊥₋; [_]; _₋; ≡-dec)
+open import Relation.Nullary.Decidable.Core using (yes; no; map′)
 import Relation.Nullary.Decidable.Core as Dec using (map′)
 
 ------------------------------------------------------------------------

src/Relation/Binary/Construct/Add/Infimum/Strict.agda

@@ -30,10 +30,9 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (Asymmetric; Transitive; Decidable; Irrelevant; Irreflexive; Trans
         ; Trichotomous; tri≈; tri<; tri>; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
-open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Infimum
   using (⊥₋; [_]; _₋; ≡-dec; []-injective)
-import Relation.Nullary.Decidable.Core as Dec using (map′)
+open import Relation.Nullary.Decidable.Core as Dec using (yes; no; map′)
 
 ------------------------------------------------------------------------
 -- Definition