Recomputable

src/Relation/Binary/Consequences.agda

@@ -11,7 +11,7 @@ module Relation.Binary.Consequences where
 open import Data.Maybe.Base using (just; nothing)
 open import Data.Sum as Sum using (inj₁; inj₂)
 open import Data.Product using (_,_)
-open import Data.Empty using (⊥-elim)
+open import Data.Empty.Irrelevant using (⊥-elim)
 open import Function using (_∘_; flip)
 open import Level using (Level)
 open import Relation.Binary.Core
@@ -164,3 +164,9 @@ module _ {P : REL A B ℓ₁} {Q : REL B A ℓ₂} where
 
   flip-Connex : Connex P Q → Connex Q P
   flip-Connex f x y = Sum.swap (f y x)
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+     dec⟶irrel′ : Decidable R → Irrelevant′ R
+     dec⟶irrel′ dec {a} {b} _ with dec a b
+     dec⟶irrel′ _ _ | yes p = p
+     dec⟶irrel′ _ r | no ¬p = ⊥-elim (¬p r)

src/Relation/Binary/Core.agda

@@ -217,6 +217,12 @@ 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
+-- irrelevant one.
+
+Irrelevant′ : REL A B ℓ → Set _
+Irrelevant′ _∼_ = ∀ {x y} → .(x ∼ y) → x ∼ y
+
 -- Universal - all pairs of elements are related
 
 Universal : REL A B ℓ → Set _