From 4d59253632f39c3f18f1cf7fa1620c8720928bf6 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sat, 25 May 2019 16:24:07 -0400
Subject: [PATCH 1/5] the result of decision procedure is fixed once witnessed
 is provided

---
 CHANGELOG.md                         | 14 ++++++++++++++
 src/Relation/Nullary/Decidable.agda  | 20 +++++++++++++++++++-
 src/Relation/Nullary/Irrelevant.agda | 14 ++++++++++++++
 3 files changed, 47 insertions(+), 1 deletion(-)
 create mode 100644 src/Relation/Nullary/Irrelevant.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b72b90f897..f5bfa18869 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -644,3 +644,17 @@ Other minor additions
                           (isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε)
 
   ```
+
+* Added a new module `Relation.Nullary.Irrelvant`:
+  ```agda
+  Irrelevant : ∀ {p} → Set p → Set p
+  Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
+  ```
+  
+* Added three lemmas in `Relation.Nullary.Decidable` which constraints the output of
+  decision procedures:
+  ```agda
+  p?-yes : ∀ (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
+  p?-no : ∀ (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+  p?-yes-irr : ∀ (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
+  ```
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 0a535ac5be..e7549ca835 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -21,6 +21,7 @@ open import Level using (Level; Lift)
 open import Relation.Binary using (Setoid; module Setoid; Decidable)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary
+open import Relation.Nullary.Irrelevant
 
 private
   variable
@@ -92,7 +93,7 @@ module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} whe
 ------------------------------------------------------------------------
 -- Extracting proofs
 
-module _ {p} {P : Set p} where
+module _ {P : Set p} where
 
 -- If a decision procedure returns "yes", then we can extract the
 -- proof using from-yes.
@@ -115,3 +116,20 @@ module _ {p} {P : Set p} where
   from-no : (p : Dec P) → From-no p
   from-no (no ¬p) = ¬p
   from-no (yes _) = _
+
+------------------------------------------------------------------------
+-- Result of decidability
+
+module _ {P : Set p} where
+
+  p?-yes : ∀ (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
+  p?-yes (yes p′) p = p′ , refl
+  p?-yes (no ¬p) p = ⊥-elim (¬p p)
+
+  p?-no : ∀ (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+  p?-no (yes p) ¬p  = ¬p , ⊥-elim (¬p p)
+  p?-no (no ¬p′) ¬p = ¬p′ , refl
+
+  p?-yes-irr : ∀ (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
+  p?-yes-irr p? irr p with p?-yes p? p
+  ... | p′ , eq rewrite irr p p′ = eq
diff --git a/src/Relation/Nullary/Irrelevant.agda b/src/Relation/Nullary/Irrelevant.agda
new file mode 100644
index 0000000000..722a22204b
--- /dev/null
+++ b/src/Relation/Nullary/Irrelevant.agda
@@ -0,0 +1,14 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Nullary irrelevance
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Nullary.Irrelevant where
+
+open import Relation.Binary.PropositionalEquality
+
+Irrelevant : ∀ {p} → Set p → Set p
+Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂

From 6aea8c8022cf2ad2e27c1d48efe4e0a1d48706f1 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sun, 26 May 2019 10:04:19 -0400
Subject: [PATCH 2/5] fix whitespace

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index f5bfa18869..0c7e265c23 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -650,7 +650,7 @@ Other minor additions
   Irrelevant : ∀ {p} → Set p → Set p
   Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
   ```
-  
+
 * Added three lemmas in `Relation.Nullary.Decidable` which constraints the output of
   decision procedures:
   ```agda

From f72bb78401f9f077eec790c9a383a82782eb3d82 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Wed, 29 May 2019 12:11:44 -0400
Subject: [PATCH 3/5] comment

---
 CHANGELOG.md                        |  9 ++++-----
 src/Relation/Nullary/Decidable.agda | 22 ++++++++++------------
 2 files changed, 14 insertions(+), 17 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0c7e265c23..9040b1bc9b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -645,16 +645,15 @@ Other minor additions
 
   ```
 
-* Added a new module `Relation.Nullary.Irrelvant`:
+* Added a new module `Relation.Nullary.Irrelevant`:
   ```agda
-  Irrelevant : ∀ {p} → Set p → Set p
   Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
   ```
 
 * Added three lemmas in `Relation.Nullary.Decidable` which constraints the output of
   decision procedures:
   ```agda
-  p?-yes : ∀ (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
-  p?-no : ∀ (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
-  p?-yes-irr : ∀ (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
+  dec-yes     : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
+  dec-no      : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+  dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
   ```
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index e7549ca835..65cf85f553 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -93,7 +93,7 @@ module _ {a₁ a₂ b₁ b₂} {A : Setoid a₁ a₂} {B : Setoid b₁ b₂} whe
 ------------------------------------------------------------------------
 -- Extracting proofs
 
-module _ {P : Set p} where
+module _ {p} {P : Set p} where
 
 -- If a decision procedure returns "yes", then we can extract the
 -- proof using from-yes.
@@ -120,16 +120,14 @@ module _ {P : Set p} where
 ------------------------------------------------------------------------
 -- Result of decidability
 
-module _ {P : Set p} where
+dec-yes : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
+dec-yes (yes p′) p = p′ , refl
+dec-yes (no ¬p) p = ⊥-elim (¬p p)
 
-  p?-yes : ∀ (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
-  p?-yes (yes p′) p = p′ , refl
-  p?-yes (no ¬p) p = ⊥-elim (¬p p)
+dec-no : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+dec-no (yes p) ¬p  = ¬p , ⊥-elim (¬p p)
+dec-no (no ¬p′) ¬p = ¬p′ , refl
 
-  p?-no : ∀ (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
-  p?-no (yes p) ¬p  = ¬p , ⊥-elim (¬p p)
-  p?-no (no ¬p′) ¬p = ¬p′ , refl
-
-  p?-yes-irr : ∀ (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
-  p?-yes-irr p? irr p with p?-yes p? p
-  ... | p′ , eq rewrite irr p p′ = eq
+dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
+dec-yes-irr p? irr p with dec-yes p? p
+... | p′ , eq rewrite irr p p′ = eq

From 8cbd3b36f503b2ebe2d358e04dc0463b2687173e Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Wed, 29 May 2019 13:12:50 -0400
Subject: [PATCH 4/5] move irrelevant to nullary

---
 CHANGELOG.md                                       |  2 +-
 src/Axiom/UniquenessOfIdentityProofs.agda          |  2 +-
 src/Data/List/Relation/Binary/Pointwise.agda       |  2 +-
 src/Data/List/Relation/Unary/All.agda              |  2 +-
 src/Data/Maybe/Relation/Unary/All.agda             |  2 +-
 src/Data/Maybe/Relation/Unary/Any.agda             |  2 +-
 src/Data/Nat/Properties.agda                       |  2 +-
 src/Data/Vec/Relation/Unary/All.agda               |  2 +-
 .../Binary/Construct/Add/Extrema/Strict.agda       |  2 +-
 .../Binary/Construct/Add/Infimum/NonStrict.agda    |  2 +-
 .../Binary/Construct/Add/Infimum/Strict.agda       |  2 +-
 .../Binary/Construct/Add/Point/Equality.agda       |  2 +-
 .../Binary/Construct/Add/Supremum/NonStrict.agda   |  2 +-
 .../Binary/Construct/Add/Supremum/Strict.agda      |  2 +-
 src/Relation/Binary/HeterogeneousEquality.agda     |  2 +-
 src/Relation/Nullary.agda                          |  5 +++++
 src/Relation/Nullary/Decidable.agda                |  3 +--
 src/Relation/Nullary/Irrelevant.agda               | 14 --------------
 src/Relation/Unary.agda                            |  2 +-
 19 files changed, 22 insertions(+), 32 deletions(-)
 delete mode 100644 src/Relation/Nullary/Irrelevant.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9040b1bc9b..b3494d94d8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -645,7 +645,7 @@ Other minor additions
 
   ```
 
-* Added a new module `Relation.Nullary.Irrelevant`:
+* Added the definition for `Irrelevant` in `Relation.Nullary`:
   ```agda
   Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
   ```
diff --git a/src/Axiom/UniquenessOfIdentityProofs.agda b/src/Axiom/UniquenessOfIdentityProofs.agda
index ab0bdc2366..555e7e9477 100644
--- a/src/Axiom/UniquenessOfIdentityProofs.agda
+++ b/src/Axiom/UniquenessOfIdentityProofs.agda
@@ -9,7 +9,7 @@
 module Axiom.UniquenessOfIdentityProofs where
 
 open import Data.Empty
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core
 
diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda
index 9805fa5154..8ccc4e07c5 100644
--- a/src/Data/List/Relation/Binary/Pointwise.agda
+++ b/src/Data/List/Relation/Binary/Pointwise.agda
@@ -16,7 +16,7 @@ open import Data.List.Properties using (≡-dec)
 open import Data.Fin using (Fin) renaming (zero to fzero; suc to fsuc)
 open import Data.Nat using (ℕ; zero; suc)
 open import Level
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Negation using (contradiction)
 import Relation.Nullary.Decidable as Dec using (map′)
 open import Relation.Unary as U using (Pred)
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index d29171b9c4..55ff77cfce 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -16,7 +16,7 @@ open import Data.List.Membership.Propositional using (_∈_)
 open import Data.Product as Prod using (∃; -,_; _×_; _,_; proj₁; proj₂)
 open import Function
 open import Level
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Unary hiding (_∈_)
 open import Relation.Binary.PropositionalEquality as P
diff --git a/src/Data/Maybe/Relation/Unary/All.agda b/src/Data/Maybe/Relation/Unary/All.agda
index 24d890ff20..f4a73dfc50 100644
--- a/src/Data/Maybe/Relation/Unary/All.agda
+++ b/src/Data/Maybe/Relation/Unary/All.agda
@@ -18,7 +18,7 @@ open import Function.Equivalence using (_⇔_; equivalence)
 open import Level
 open import Relation.Binary.PropositionalEquality as P using (_≡_; cong)
 open import Relation.Unary
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Maybe/Relation/Unary/Any.agda b/src/Data/Maybe/Relation/Unary/Any.agda
index 714e6fc985..98c87a31db 100644
--- a/src/Data/Maybe/Relation/Unary/Any.agda
+++ b/src/Data/Maybe/Relation/Unary/Any.agda
@@ -15,7 +15,7 @@ open import Function.Equivalence using (_⇔_; equivalence)
 open import Level
 open import Relation.Binary.PropositionalEquality as P using (_≡_; cong)
 open import Relation.Unary
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index e07f28aeb4..aad2741605 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -28,7 +28,7 @@ open import Level using (0ℓ)
 open import Relation.Binary
 open import Relation.Binary.Consequences using (flip-Connex)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Decidable using (True; via-injection; map′)
 open import Relation.Nullary.Negation using (contradiction)
 
diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda
index 9779a8c652..41eb877328 100644
--- a/src/Data/Vec/Relation/Unary/All.agda
+++ b/src/Data/Vec/Relation/Unary/All.agda
@@ -14,7 +14,7 @@ open import Data.Product as Prod using (_,_)
 open import Data.Vec as Vec using (Vec; []; _∷_)
 open import Function using (_∘_)
 open import Level using (Level; _⊔_)
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Unary
 open import Relation.Binary.PropositionalEquality as P using (subst)
diff --git a/src/Relation/Binary/Construct/Add/Extrema/Strict.agda b/src/Relation/Binary/Construct/Add/Extrema/Strict.agda
index b676458e09..e288c548ed 100644
--- a/src/Relation/Binary/Construct/Add/Extrema/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Extrema/Strict.agda
@@ -16,7 +16,7 @@ module Relation.Binary.Construct.Add.Extrema.Strict
 
 open import Level
 open import Function
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 
 import Relation.Nullary.Construct.Add.Infimum as I
 open import Relation.Nullary.Construct.Add.Extrema
diff --git a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
index 34db09c3c0..e4cd888134 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
@@ -19,7 +19,7 @@ open import Data.Sum as Sum
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; refl)
 import Relation.Binary.Construct.Add.Infimum.Equality as Equality
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Infimum
 import Relation.Nullary.Decidable as Dec
 
diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
index 61813f7d15..14e2d2a8cd 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
@@ -21,7 +21,7 @@ open import Relation.Binary.PropositionalEquality as P
   using (_≡_; refl)
 import Relation.Binary.Construct.Add.Infimum.Equality as Equality
 import Relation.Binary.Construct.Add.Infimum.NonStrict as NonStrict
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Infimum
 import Relation.Nullary.Decidable as Dec
 
diff --git a/src/Relation/Binary/Construct/Add/Point/Equality.agda b/src/Relation/Binary/Construct/Add/Point/Equality.agda
index 42ce4591bc..3d072e6d54 100644
--- a/src/Relation/Binary/Construct/Add/Point/Equality.agda
+++ b/src/Relation/Binary/Construct/Add/Point/Equality.agda
@@ -17,7 +17,7 @@ module Relation.Binary.Construct.Add.Point.Equality
 open import Level using (_⊔_)
 open import Function
 import Relation.Binary.PropositionalEquality as P
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Point
 import Relation.Nullary.Decidable as Dec
 
diff --git a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
index 28a41256ad..f2900a82eb 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
@@ -16,7 +16,7 @@ module Relation.Binary.Construct.Add.Supremum.NonStrict
 
 open import Level using (_⊔_)
 open import Data.Sum as Sum
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; refl)
diff --git a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
index 8bd9d93722..2fdaf2d2bd 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
@@ -17,7 +17,7 @@ module Relation.Binary.Construct.Add.Supremum.Strict
 open import Level using (_⊔_)
 open import Data.Product
 open import Function
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; refl)
diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda
index 9ea77883b1..31796cc05d 100644
--- a/src/Relation/Binary/HeterogeneousEquality.agda
+++ b/src/Relation/Binary/HeterogeneousEquality.agda
@@ -14,7 +14,7 @@ open import Data.Unit.NonEta
 open import Function
 open import Function.Inverse using (Inverse)
 open import Level
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Unary using (Pred)
 open import Relation.Binary
 open import Relation.Binary.Consequences
diff --git a/src/Relation/Nullary.agda b/src/Relation/Nullary.agda
index 74d26ecc73..1ed5246327 100644
--- a/src/Relation/Nullary.agda
+++ b/src/Relation/Nullary.agda
@@ -10,6 +10,8 @@
 
 module Relation.Nullary where
 
+open import Agda.Builtin.Equality
+
 open import Data.Empty hiding (⊥-elim)
 open import Data.Empty.Irrelevant
 open import Level
@@ -32,3 +34,6 @@ data Dec {p} (P : Set p) : Set p where
 recompute : ∀ {a} {A : Set a} → Dec A → .A → A
 recompute (yes x) _ = x
 recompute (no ¬p) x = ⊥-elim (¬p x)
+
+Irrelevant : ∀ {p} → Set p → Set p
+Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 65cf85f553..b5cda46ae2 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -19,9 +19,8 @@ open import Function.Equivalence
 open import Function.Injection using (Injection; module Injection)
 open import Level using (Level; Lift)
 open import Relation.Binary using (Setoid; module Setoid; Decidable)
-open import Relation.Binary.PropositionalEquality
+open import Agda.Builtin.Equality
 open import Relation.Nullary
-open import Relation.Nullary.Irrelevant
 
 private
   variable
diff --git a/src/Relation/Nullary/Irrelevant.agda b/src/Relation/Nullary/Irrelevant.agda
deleted file mode 100644
index 722a22204b..0000000000
--- a/src/Relation/Nullary/Irrelevant.agda
+++ /dev/null
@@ -1,14 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Nullary irrelevance
-------------------------------------------------------------------------
-
-{-# OPTIONS --without-K --safe #-}
-
-module Relation.Nullary.Irrelevant where
-
-open import Relation.Binary.PropositionalEquality
-
-Irrelevant : ∀ {p} → Set p → Set p
-Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 3804748c7c..3486a03fcf 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -14,7 +14,7 @@ open import Data.Product
 open import Data.Sum using (_⊎_; [_,_])
 open import Function
 open import Level
-open import Relation.Nullary
+open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 private

From 21fba3e89d0427165dbbcac5bc0465505600e7f7 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sat, 1 Jun 2019 09:58:40 -0400
Subject: [PATCH 5/5] merge from master

---
 CHANGELOG.md                                   |  2 +-
 src/Relation/Binary/PropositionalEquality.agda |  9 +++------
 src/Relation/Nullary/Decidable/Core.agda       | 18 ++++++++++++++++++
 3 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2e5ebbf089..0a49ece5ba 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -703,7 +703,7 @@ Other minor additions
   Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
   ```
 
-* Added three lemmas in `Relation.Nullary.Decidable` which constraints the output of
+* Added three lemmas in `Relation.Nullary.Decidable.Core` which constraints the output of
   decision procedures:
   ```agda
   dec-yes     : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index b301d4f3c2..1aebf4e487 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/src/Relation/Binary/PropositionalEquality.agda
@@ -20,6 +20,7 @@ open import Data.Product
 open import Function.Nary.NonDependent
 
 open import Relation.Nullary using (yes ; no)
+open import Relation.Nullary.Decidable.Core
 open import Relation.Unary using (Pred)
 open import Relation.Binary
 open import Relation.Binary.Indexed.Heterogeneous
@@ -233,14 +234,10 @@ cong-≡id {f = f} {x} f≡id =
 module _ (_≟_ : Decidable {A = A} _≡_) where
 
   ≡-≟-identity : ∀ {x y : A} (eq : x ≡ y) → x ≟ y ≡ yes eq
-  ≡-≟-identity {x} {y} eq with x ≟ y
-  ... | yes p = cong yes (Decidable⇒UIP.≡-irrelevant _≟_ p eq)
-  ... | no ¬p = ⊥-elim (¬p eq)
+  ≡-≟-identity {x} {y} eq = dec-yes-irr (x ≟ y) (Decidable⇒UIP.≡-irrelevant _≟_) eq
 
   ≢-≟-identity : ∀ {x y : A} → x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq
-  ≢-≟-identity {x} {y} ¬eq with x ≟ y
-  ... | yes p = ⊥-elim (¬eq p)
-  ... | no ¬p = ¬p , refl
+  ≢-≟-identity {x} {y} ¬eq = dec-no (x ≟ y) ¬eq
 
 
 
diff --git a/src/Relation/Nullary/Decidable/Core.agda b/src/Relation/Nullary/Decidable/Core.agda
index b940d1176f..fc8ad80759 100644
--- a/src/Relation/Nullary/Decidable/Core.agda
+++ b/src/Relation/Nullary/Decidable/Core.agda
@@ -14,8 +14,11 @@ 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.Unit.Base using (⊤)
+open import Data.Empty
+open import Data.Product
 open import Function
 
+open import Agda.Builtin.Equality
 open import Relation.Nullary
 
 private
@@ -79,3 +82,18 @@ module _ {p} {P : Set p} where
   from-no : (p : Dec P) → From-no p
   from-no (no ¬p) = ¬p
   from-no (yes _) = _
+
+------------------------------------------------------------------------
+-- Result of decidability
+
+dec-yes : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
+dec-yes (yes p′) p = p′ , refl
+dec-yes (no ¬p) p = ⊥-elim (¬p p)
+
+dec-no : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+dec-no (yes p) ¬p  = ¬p , ⊥-elim (¬p p)
+dec-no (no ¬p′) ¬p = ¬p′ , refl
+
+dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
+dec-yes-irr p? irr p with dec-yes p? p
+... | p′ , eq rewrite irr p p′ = eq