[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 <[email protected]>

* Fix

* Update CHANGELOG.md

Co-authored-by: jamesmckinna <[email protected]>

---------

Co-authored-by: Jacques Carette <[email protected]>
Co-authored-by: jamesmckinna <[email protected]>

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

src/Relation/Binary/HeterogeneousEquality.agda

@@ -12,8 +12,6 @@ open import Data.Product.Base using (_,_)
 open import Function.Base using (case_of_; _∋_; id)
 open import Function.Bundles using (Inverse)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary hiding (Irrelevant)
-open import Relation.Unary using (Pred)
 open import Relation.Binary.Core using (Rel; REL; _⇒_)
 open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder)
 open import Relation.Binary.Structures using (IsEquivalence; IsPreorder)
@@ -26,6 +24,9 @@ open import Relation.Binary.Indexed.Heterogeneous.Construct.At
   using (_atₛ_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
 open import Relation.Binary.Reasoning.Syntax
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Unary using (Pred)
 
 import Relation.Binary.PropositionalEquality.Properties as ≡
 import Relation.Binary.HeterogeneousEquality.Core as Core

src/Relation/Binary/PropositionalEquality.agda

@@ -13,7 +13,7 @@ open import Function.Base using (id; _∘_)
 import Function.Dependent.Bundles as Dependent using (Func)
 open import Function.Indexed.Relation.Binary.Equality using (≡-setoid)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary using (Irrelevant)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Nullary.Decidable using (yes; no; dec-yes-irr; dec-no)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions using (DecidableEquality)

src/Relation/Nullary.agda

@@ -27,12 +27,7 @@ open import Relation.Nullary.Recomputable public using (Recomputable)
 open import Relation.Nullary.Negation.Core public
 open import Relation.Nullary.Reflects public hiding (recompute; recompute-constant)
 open import Relation.Nullary.Decidable.Core public
-
-------------------------------------------------------------------------
--- Irrelevant types
-
-Irrelevant : Set p → Set p
-Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
+open import Relation.Nullary.Irrelevant public
 
 ------------------------------------------------------------------------
 -- Weak decidability

src/Relation/Nullary/Decidable.agda

@@ -15,7 +15,7 @@ open import Function.Bundles
   using (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔ₛ′)
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary using (Irrelevant)
+open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Binary.PropositionalEquality.Core

src/Relation/Nullary/Irrelevant.agda

@@ -0,0 +1,20 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A type `A` is irrelevant if all of its elements are equal.
+-- This is also refered to as "A is an h-proposition".
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Nullary.Irrelevant where
+
+open import Agda.Builtin.Equality using (_≡_)
+open import Level using (Level)
+
+private
+  variable
+    p : Level
+
+Irrelevant : Set p → Set p
+Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂