From 5741c80877e7d3ffcee9a842804ccb794719d3d3 Mon Sep 17 00:00:00 2001
From: M Farkas-Dyck <strake888@gmail.com>
Date: Tue, 7 May 2019 11:30:15 -0500
Subject: [PATCH 1/6] =?UTF-8?q?irrelevance=E2=80=B2?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Relation/Binary/Consequences.agda | 8 +++++++-
 src/Relation/Binary/Core.agda         | 6 ++++++
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 1b2f079d51..2cdb73051a 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/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)
diff --git a/src/Relation/Binary/Core.agda b/src/Relation/Binary/Core.agda
index f8612dc9e9..54541b168d 100644
--- a/src/Relation/Binary/Core.agda
+++ b/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 _

From 50276fe6b23525beb332725d60a292aaee325377 Mon Sep 17 00:00:00 2001
From: M Farkas-Dyck <strake888@gmail.com>
Date: Thu, 9 May 2019 07:27:40 -0500
Subject: [PATCH 2/6] clean up

---
 src/Relation/Binary/Consequences.agda | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 2cdb73051a..266bc80b75 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -12,10 +12,10 @@ 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.Irrelevant using (⊥-elim)
-open import Function using (_∘_; flip)
+open import Function using (_∘_; _$_; flip)
 open import Level using (Level)
 open import Relation.Binary.Core
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary using (yes; no; recompute)
 open import Relation.Unary using (∁)
 
 private
@@ -165,8 +165,7 @@ 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
+module _ {r} {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)
+     dec⟶irrel′ dec {a} {b} = recompute $ dec a b

From 6daa0fb625b6417cafe32989e63ce2d11a787f67 Mon Sep 17 00:00:00 2001
From: M Farkas-Dyck <strake888@gmail.com>
Date: Thu, 9 May 2019 08:06:56 -0500
Subject: [PATCH 3/6] log changes

---
 CHANGELOG.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4be30f987e..323ef748d1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -307,3 +307,11 @@ Other minor additions
   ```agda
   ≢-sym : Symmetric _≢_
   ```
+
+* Defined another notion of irrelevance (reconstructibility) for binary relations:
+  ```agda
+  Irrelevant′ : REL A B ℓ → Set _
+  Irrelevant′ _~_ = ∀ {x y} → .(x ~ y) → x ~ y
+
+  dec⟶irrel′ : Decidable R → Irrelevant′ R
+  ```

From 1f1eaf5523dbcd7708a6327bf2c81070ad7f1e1b Mon Sep 17 00:00:00 2001
From: M Farkas-Dyck <strake888@gmail.com>
Date: Sun, 12 May 2019 10:41:40 -0500
Subject: [PATCH 4/6] =?UTF-8?q?rename=20`Irrelevant=E2=80=B2`=20as=20`Reco?=
 =?UTF-8?q?mputable`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                          | 8 ++++----
 src/Relation/Binary/Consequences.agda | 4 ++--
 src/Relation/Binary/Core.agda         | 6 +++---
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 323ef748d1..9397c799cd 100644
--- a/CHANGELOG.md
+++ b/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
   ```
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 266bc80b75..d3a572f6e3 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/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
diff --git a/src/Relation/Binary/Core.agda b/src/Relation/Binary/Core.agda
index 54541b168d..b54096205e 100644
--- a/src/Relation/Binary/Core.agda
+++ 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
 

From 7c4acc1120f434815ce6ecb35700c7576c272979 Mon Sep 17 00:00:00 2001
From: M Farkas-Dyck <strake888@gmail.com>
Date: Sun, 12 May 2019 10:41:40 -0500
Subject: [PATCH 5/6] =?UTF-8?q?rename=20`Irrelevant=E2=80=B2`=20as=20`Reco?=
 =?UTF-8?q?mputable`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                          | 10 +++++++++-
 src/Relation/Binary/Consequences.agda |  4 ++--
 2 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 65a623aa69..beef8d60f6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -466,4 +466,12 @@ Other minor additions
 * Added new notation to `Relation.Unary`:
   ```agda
   syntax Satisfiable P = ∃⟨ P ⟩
-  ```
\ No newline at end of file
+  ```
+
+* Defined a notion of recomputability for binary relations:
+  ```agda
+  Recomputable : REL A B ℓ → Set _
+  Recomputable _~_ = ∀ {x y} → .(x ~ y) → x ~ y
+
+  dec⟶recomputable : Decidable R → Recomputable R
+  ```
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index d3a572f6e3..6ea4fafb57 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/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⟶recomput : Decidable R → Recomputable R
-     dec⟶recomput dec {a} {b} = recompute $ dec a b
+     dec⟶recomputable : Decidable R → Recomputable R
+     dec⟶recomputable dec {a} {b} = recompute $ dec a b

From 755e0aef4a4d036ba5689ddccdb572376d5c2eb6 Mon Sep 17 00:00:00 2001
From: M Farkas-Dyck <strake888@gmail.com>
Date: Sun, 12 May 2019 22:15:49 -0500
Subject: [PATCH 6/6] define recomputability of unary relations

---
 CHANGELOG.md                         |  9 ++++++++-
 src/Relation/Unary.agda              |  6 ++++++
 src/Relation/Unary/Consequences.agda | 15 +++++++++++++++
 3 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 src/Relation/Unary/Consequences.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index beef8d60f6..755bbecafb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -468,7 +468,14 @@ Other minor additions
   syntax Satisfiable P = ∃⟨ P ⟩
   ```
 
-* Defined a notion of recomputability for binary relations:
+* Defined a notion of recomputability for unary and binary relations:
+  ```agda
+  Recomputable : Pred A ℓ → Set _
+  Recomputable P = ∀ {x} → .(P x) → P x
+
+  dec⟶recomputable : Decidable P → Recomputable P
+  ```
+
   ```agda
   Recomputable : REL A B ℓ → Set _
   Recomputable _~_ = ∀ {x y} → .(x ~ y) → x ~ y
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 7cb42a2fd9..3804748c7c 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -167,6 +167,12 @@ Decidable P = ∀ x → Dec (P x)
 Irrelevant : Pred A ℓ → Set _
 Irrelevant P = ∀ {x} (a : P x) (b : P x) → a ≡ b
 
+-- Recomputability - we can rebuild a relevant proof given an
+-- irrelevant one.
+
+Recomputable : Pred A ℓ → Set _
+Recomputable P = ∀ {x} → .(P x) → P x
+
 ------------------------------------------------------------------------
 -- Operations on sets
 
diff --git a/src/Relation/Unary/Consequences.agda b/src/Relation/Unary/Consequences.agda
new file mode 100644
index 0000000000..23bf21b22d
--- /dev/null
+++ b/src/Relation/Unary/Consequences.agda
@@ -0,0 +1,15 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some properties imply others
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Unary.Consequences where
+
+open import Relation.Unary
+open import Relation.Nullary using (recompute)
+
+dec⟶recomputable : {a ℓ : _} {A : Set a} {P : Pred A ℓ} → Decidable P → Recomputable P
+dec⟶recomputable P-dec = recompute (P-dec _)