rename Irrelevant′ as Recomputable

Author: strake

CHANGELOG.md

@@ -308,10 +308,10 @@ Other minor additions
   ≢-sym : Symmetric _≢_
   ```
 
-* Defined another notion of irrelevance (reconstructibility) for binary relations:
+* Defined a notion of recomputability for binary relations:
   ```agda
-  Irrelevant′ : REL A B ℓ → Set _
-  Irrelevant′ _~_ = ∀ {x y} → .(x ~ y) → x ~ y
+  Recomputable : REL A B ℓ → Set _
+  Recomputable _~_ = ∀ {x y} → .(x ~ y) → x ~ y
 
-  dec⟶irrel′ : Decidable R → Irrelevant′ R
+  dec⟶recomput : Decidable R → Recomputable R
   ```

src/Relation/Binary/Consequences.agda

@@ -167,5 +167,5 @@ module _ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} where
 
 module _ {r} {R : REL A B r} where
 
-     dec⟶irrel′ : Decidable R → Irrelevant′ R
-     dec⟶irrel′ dec {a} {b} = recompute $ dec a b
+     dec⟶recomput : Decidable R → Recomputable R
+     dec⟶recomput dec {a} {b} = recompute $ dec a b

src/Relation/Binary/Core.agda

@@ -217,11 +217,11 @@ WeaklyDecidable _∼_ = ∀ x y → Maybe (x ∼ y)
 Irrelevant : REL A B ℓ → Set _
 Irrelevant _∼_ = ∀ {x y} (a b : x ∼ y) → a ≡ b
 
--- Another irrelevancy - we can rebuild a relevant proof given an
+-- Recomputability - we can rebuild a relevant proof given an
 -- irrelevant one.
 
-Irrelevant′ : REL A B ℓ → Set _
-Irrelevant′ _∼_ = ∀ {x y} → .(x ∼ y) → x ∼ y
+Recomputable : REL A B ℓ → Set _
+Recomputable _∼_ = ∀ {x y} → .(x ∼ y) → x ∼ y
 
 -- Universal - all pairs of elements are related