the result of decision procedure is fixed once witnessed is provided

CHANGELOG.md

@@ -697,3 +697,16 @@ Other minor additions
                           (isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε)
 
   ```
+
+* Added the definition for `Irrelevant` in `Relation.Nullary`:
+  ```agda
+  Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
+  ```
+
+* 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′
+  dec-no      : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+  dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
+  ```

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
 

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)

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

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

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

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)
 

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)

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

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
 

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
 

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
 

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)

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)

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

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
 
 
 

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₂

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

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