irrelevance of recompute

Author: jamesmckinna

CHANGELOG.md

@@ -407,6 +407,11 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
+* Added new proof in `Relation.Nullary.Decidable.Core`:
+  ```agda
+  recompute-irr : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+  ```
+
 * Added new proof in `Relation.Nullary.Decidable`:
   ```agda
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
@@ -419,13 +424,8 @@ Additions to existing modules
 
 * Added new definitions in `Relation.Nullary.Reflects`:
   ```agda
-  recompute : Reflects A b → Recomputable A
-  ```
-
-* Added new definitions in `Relation.Unary`
-  ```
-  Stable          : Pred A ℓ → Set _
-  WeaklyDecidable : Pred A ℓ → Set _
+  recompute     : Reflects A b → Recomputable A
+  recompute-irr : (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
   ```
 
 * Added new definitions in `Relation.Unary`

src/Relation/Nullary/Decidable/Core.agda

@@ -18,9 +18,10 @@ open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_∘_; const; _$_; flip)
 open import Relation.Nullary.Recomputable
-open import Relation.Nullary.Reflects as Reflects hiding (recompute)
+open import Relation.Nullary.Reflects as Reflects hiding (recompute; recompute-irr)
 open import Relation.Nullary.Negation.Core
   using (¬_; Stable; negated-stable; contradiction; DoubleNegation)
+open import Agda.Builtin.Equality using (_≡_)
 
 private
   variable
@@ -73,6 +74,9 @@ module _ {A : Set a} where
 recompute : Dec A → Recomputable A
 recompute = Reflects.recompute ∘ proof
 
+recompute-irr : (a? : Dec A) (p q : A) → recompute a? p ≡ recompute a? q
+recompute-irr = Reflects.recompute-irr ∘ proof
+
 ------------------------------------------------------------------------
 -- Interaction with negation, sum, product etc.
 

src/Relation/Nullary/Reflects.agda

@@ -61,6 +61,9 @@ recompute : ∀ {b} → Reflects A b → Recomputable A
 recompute (ofʸ  a) _ = a
 recompute (ofⁿ ¬a) a = contradiction-irr a ¬a
 
+recompute-irr : ∀ {b} (r : Reflects A b) (p q : A) → recompute r p ≡ recompute r q
+recompute-irr r p q = refl
+
 ------------------------------------------------------------------------
 -- Interaction with negation, product, sums etc.