From 1b7c0b32a9a241accaae74ba66694f0c3309d913 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Sun, 7 Jul 2024 23:07:47 +0200
Subject: [PATCH 1/7] Add proofs on truth value
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Adds a handful of properties that prove the truth
value of a decidable:

- `Relation.Nullary.Decidable`:
  - `does-≡`: decidables over the same type have the same truth value
  - `does-⇔`: generalization of `does-≡` to mutually implied types

- `Relation.Unary.Properties`:
  - `≐?`: generalization of `Decidable.map` to predicates
    (if two predicates are equivalent, one is decidable if the other is)
  - `does-≡`: generalization of `does-≡` to predicates
  - `does-≐`: generalization of `does-⇔` to predicates
---
 CHANGELOG.md                        | 11 ++++++++++-
 src/Relation/Nullary/Decidable.agda | 10 +++++++++-
 src/Relation/Unary/Properties.agda  | 19 +++++++++++++++++--
 3 files changed, 36 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d5851dde0d..6be2adb7a7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -800,9 +800,11 @@ Additions to existing modules
   WeaklyDecidable : Set _
   ```
 
-* Added new proof in `Relation.Nullary.Decidable`:
+* Added new proofs in `Relation.Nullary.Decidable`:
   ```agda
   ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋
+  does-⇔  : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
+  does-≡  : (a? b? : Dec A) → does a? ≡ does b?
   ```
 
 * Added new definitions and proofs in `Relation.Nullary.Decidable.Core`:
@@ -830,6 +832,13 @@ Additions to existing modules
   WeaklyDecidable : Pred A ℓ → Set _
   ```
 
+* Added new proofs in `Relation.Nullary.Properties`:
+  ```agda
+  ≐?     : P ≐ Q → Decidable P → Decidable Q
+  does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?
+  does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′
+  ```
+
 * Enhancements to `Tactic.Cong` - see `README.Tactic.Cong` for details.
   - Provide a marker function, `⌞_⌟`, for user-guided anti-unification.
   - Improved support for equalities between terms with instance arguments,
diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 4b28ed43f1..4617191fe2 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -11,8 +11,9 @@ module Relation.Nullary.Decidable where
 open import Level using (Level)
 open import Data.Bool.Base using (true; false)
 open import Data.Product.Base using (∃; _,_)
+open import Function.Base using (id; _∘_)
 open import Function.Bundles using
-  (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔ₛ′)
+  (Injection; module Injection; module Equivalence; _⇔_; mk⇔; _↔_; mk↔ₛ′)
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (Irrelevant)
@@ -80,3 +81,10 @@ dec-yes-irr a? irr a with a′ , eq ← dec-yes a? a rewrite irr a a′ = eq
 
 ⌊⌋-map′ : ∀ t f (a? : Dec A) → ⌊ map′ {B = B} t f a? ⌋ ≡ ⌊ a? ⌋
 ⌊⌋-map′ t f a? = trans (isYes≗does (map′ t f a?)) (sym (isYes≗does a?))
+
+does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
+does-⇔ A⇔B a? (yes b) = dec-true a? (Equivalence.from A⇔B b)
+does-⇔ A⇔B a? (no ¬b) = dec-false a? (¬b ∘ Equivalence.to A⇔B)
+
+does-≡ : (a? b? : Dec A) → does a? ≡ does b?
+does-≡ = does-⇔ (mk⇔ id id)
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index 874869e271..cb321d4eac 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -8,6 +8,7 @@
 
 module Relation.Unary.Properties where
 
+open import Data.Bool.Base using (not)
 open import Data.Product.Base as Product using (_×_; _,_; swap; proj₁; zip′)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Unit.Base using (tt)
@@ -15,10 +16,11 @@ open import Level using (Level)
 open import Relation.Binary.Core as Binary
 open import Relation.Binary.Definitions
   hiding (Decidable; Universal; Irrelevant; Empty)
-open import Relation.Binary.PropositionalEquality.Core using (refl)
+open import Relation.Binary.PropositionalEquality.Core using (refl; _≗_)
 open import Relation.Unary
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?)
+open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does; does-⇔)
 open import Function.Base using (id; _$_; _∘_)
+open import Function.Bundles using (mk⇔)
 
 private
   variable
@@ -200,6 +202,10 @@ U-Universal = λ _ → _
 ------------------------------------------------------------------------
 -- Decidability properties
 
+≐? : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
+     P ≐ Q → Decidable P → Decidable Q
+≐? (P⊆Q , Q⊆P) P? x = map′ P⊆Q Q⊆P (P? x)
+
 ∁? : {P : Pred A ℓ} → Decidable P → Decidable (∁ P)
 ∁? P? x = ¬? (P? x)
 
@@ -233,6 +239,15 @@ _⊎?_ P? Q? (inj₂ b) = Q? b
 _~? : {P : Pred (A × B) ℓ} → Decidable P → Decidable (P ~)
 _~? P? = P? ∘ swap
 
+does-≐ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} → P ≐ Q →
+         (P? : Decidable P) → (Q? : Decidable Q) →
+         does ∘ P? ≗ does ∘ Q?
+does-≐ (P⊆Q , Q⊆P) P? Q? x = does-⇔ (mk⇔ P⊆Q Q⊆P) (P? x) (Q? x)
+
+does-≡ : {P : Pred A ℓ} → (P? P?′ : Decidable P) →
+         does ∘ P? ≗ does ∘ P?′
+does-≡ {P} P? P?′ = does-≐ ≐-refl P? P?′
+
 ------------------------------------------------------------------------
 -- Irrelevant properties
 

From 3818d9480a3b990d4cf96c3deae41eda692f985b Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Mon, 24 Jun 2024 14:50:09 +0200
Subject: [PATCH 2/7] =?UTF-8?q?fixup!=20use=20=E2=87=94-id?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Relation/Nullary/Decidable.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 4617191fe2..738bb46bf4 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -11,9 +11,10 @@ module Relation.Nullary.Decidable where
 open import Level using (Level)
 open import Data.Bool.Base using (true; false)
 open import Data.Product.Base using (∃; _,_)
-open import Function.Base using (id; _∘_)
+open import Function.Base using (_∘_)
 open import Function.Bundles using
   (Injection; module Injection; module Equivalence; _⇔_; mk⇔; _↔_; mk↔ₛ′)
+open import Function.Construct.Identity using (⇔-id)
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (Irrelevant)
@@ -87,4 +88,4 @@ does-⇔ A⇔B a? (yes b) = dec-true a? (Equivalence.from A⇔B b)
 does-⇔ A⇔B a? (no ¬b) = dec-false a? (¬b ∘ Equivalence.to A⇔B)
 
 does-≡ : (a? b? : Dec A) → does a? ≡ does b?
-does-≡ = does-⇔ (mk⇔ id id)
+does-≡ = does-⇔ (⇔-id _)

From 10898f42daa6b1a01946eacde20a27431d9f00ea Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Tue, 25 Jun 2024 09:50:42 +0200
Subject: [PATCH 3/7] simplify

---
 src/Relation/Nullary/Decidable.agda | 14 ++++++--------
 src/Relation/Unary/Properties.agda  | 14 ++++++--------
 2 files changed, 12 insertions(+), 16 deletions(-)

diff --git a/src/Relation/Nullary/Decidable.agda b/src/Relation/Nullary/Decidable.agda
index 738bb46bf4..c6e9aebdf4 100644
--- a/src/Relation/Nullary/Decidable.agda
+++ b/src/Relation/Nullary/Decidable.agda
@@ -11,10 +11,8 @@ module Relation.Nullary.Decidable where
 open import Level using (Level)
 open import Data.Bool.Base using (true; false)
 open import Data.Product.Base using (∃; _,_)
-open import Function.Base using (_∘_)
 open import Function.Bundles using
-  (Injection; module Injection; module Equivalence; _⇔_; mk⇔; _↔_; mk↔ₛ′)
-open import Function.Construct.Identity using (⇔-id)
+  (Injection; module Injection; module Equivalence; _⇔_; _↔_; mk↔ₛ′)
 open import Relation.Binary.Bundles using (Setoid; module Setoid)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (Irrelevant)
@@ -83,9 +81,9 @@ dec-yes-irr a? irr a with a′ , eq ← dec-yes a? a rewrite irr a a′ = eq
 ⌊⌋-map′ : ∀ t f (a? : Dec A) → ⌊ map′ {B = B} t f a? ⌋ ≡ ⌊ a? ⌋
 ⌊⌋-map′ t f a? = trans (isYes≗does (map′ t f a?)) (sym (isYes≗does a?))
 
-does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
-does-⇔ A⇔B a? (yes b) = dec-true a? (Equivalence.from A⇔B b)
-does-⇔ A⇔B a? (no ¬b) = dec-false a? (¬b ∘ Equivalence.to A⇔B)
-
 does-≡ : (a? b? : Dec A) → does a? ≡ does b?
-does-≡ = does-⇔ (⇔-id _)
+does-≡ a? (yes a) = dec-true a? a
+does-≡ a? (no ¬a) = dec-false a? ¬a
+
+does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b?
+does-⇔ A⇔B a? = does-≡ (map A⇔B a?)
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index cb321d4eac..f1ee6a617b 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -8,7 +8,6 @@
 
 module Relation.Unary.Properties where
 
-open import Data.Bool.Base using (not)
 open import Data.Product.Base as Product using (_×_; _,_; swap; proj₁; zip′)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Unit.Base using (tt)
@@ -18,9 +17,8 @@ open import Relation.Binary.Definitions
   hiding (Decidable; Universal; Irrelevant; Empty)
 open import Relation.Binary.PropositionalEquality.Core using (refl; _≗_)
 open import Relation.Unary
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does; does-⇔)
+open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does) renaming (does-≡ to does-≡′)
 open import Function.Base using (id; _$_; _∘_)
-open import Function.Bundles using (mk⇔)
 
 private
   variable
@@ -239,14 +237,14 @@ _⊎?_ P? Q? (inj₂ b) = Q? b
 _~? : {P : Pred (A × B) ℓ} → Decidable P → Decidable (P ~)
 _~? P? = P? ∘ swap
 
+does-≡ : {P : Pred A ℓ} → (P? P?′ : Decidable P) →
+         does ∘ P? ≗ does ∘ P?′
+does-≡ P? P?′ x = does-≡′ (P? x) (P?′ x)
+
 does-≐ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} → P ≐ Q →
          (P? : Decidable P) → (Q? : Decidable Q) →
          does ∘ P? ≗ does ∘ Q?
-does-≐ (P⊆Q , Q⊆P) P? Q? x = does-⇔ (mk⇔ P⊆Q Q⊆P) (P? x) (Q? x)
-
-does-≡ : {P : Pred A ℓ} → (P? P?′ : Decidable P) →
-         does ∘ P? ≗ does ∘ P?′
-does-≡ {P} P? P?′ = does-≐ ≐-refl P? P?′
+does-≐ P≐Q P? = does-≡ (≐? P≐Q P?)
 
 ------------------------------------------------------------------------
 -- Irrelevant properties

From b55450914c2a9c34d1dbfc396ee34f0566e589d3 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Wed, 26 Jun 2024 11:09:41 +0200
Subject: [PATCH 4/7] fixup! use qualified import instead of renaming

---
 src/Relation/Unary/Properties.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index f1ee6a617b..0202b67dc2 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -17,7 +17,8 @@ open import Relation.Binary.Definitions
   hiding (Decidable; Universal; Irrelevant; Empty)
 open import Relation.Binary.PropositionalEquality.Core using (refl; _≗_)
 open import Relation.Unary
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does) renaming (does-≡ to does-≡′)
+import Relation.Nullary.Decidable as Dec
+open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
 open import Function.Base using (id; _$_; _∘_)
 
 private
@@ -239,7 +240,7 @@ _~? P? = P? ∘ swap
 
 does-≡ : {P : Pred A ℓ} → (P? P?′ : Decidable P) →
          does ∘ P? ≗ does ∘ P?′
-does-≡ P? P?′ x = does-≡′ (P? x) (P?′ x)
+does-≡ P? P?′ x = Dec.does-≡ (P? x) (P?′ x)
 
 does-≐ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} → P ≐ Q →
          (P? : Decidable P) → (Q? : Decidable Q) →

From 54b4bc045d1734f7d4cad5777790507e75cdc658 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Wed, 26 Jun 2024 18:13:20 +0200
Subject: [PATCH 5/7] Update src/Relation/Unary/Properties.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Relation/Unary/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index 0202b67dc2..cd23b6b1c0 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -18,7 +18,7 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core using (refl; _≗_)
 open import Relation.Unary
 import Relation.Nullary.Decidable as Dec
-open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
+open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
 open import Function.Base using (id; _$_; _∘_)
 
 private

From d84d22d238fef457a4d76d18853745c4492cc889 Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Mon, 1 Jul 2024 15:06:40 +0200
Subject: [PATCH 6/7] Update src/Relation/Unary/Properties.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 src/Relation/Unary/Properties.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index cd23b6b1c0..38e1e82fd9 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -17,7 +17,6 @@ open import Relation.Binary.Definitions
   hiding (Decidable; Universal; Irrelevant; Empty)
 open import Relation.Binary.PropositionalEquality.Core using (refl; _≗_)
 open import Relation.Unary
-import Relation.Nullary.Decidable as Dec
 open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
 open import Function.Base using (id; _$_; _∘_)
 

From f4b88e32ca6989f9650157fc83c76ba0afe312de Mon Sep 17 00:00:00 2001
From: Alba Mendez <me@alba.sh>
Date: Fri, 5 Jul 2024 17:37:32 +0200
Subject: [PATCH 7/7] =?UTF-8?q?rename=20=E2=89=90=3F=20to=20map?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 CHANGELOG.md                       | 2 +-
 src/Relation/Unary/Properties.agda | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6be2adb7a7..26af4b30b0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -834,7 +834,7 @@ Additions to existing modules
 
 * Added new proofs in `Relation.Nullary.Properties`:
   ```agda
-  ≐?     : P ≐ Q → Decidable P → Decidable Q
+  map    : P ≐ Q → Decidable P → Decidable Q
   does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?
   does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′
   ```
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index 38e1e82fd9..5a108d9081 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -200,9 +200,9 @@ U-Universal = λ _ → _
 ------------------------------------------------------------------------
 -- Decidability properties
 
-≐? : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
-     P ≐ Q → Decidable P → Decidable Q
-≐? (P⊆Q , Q⊆P) P? x = map′ P⊆Q Q⊆P (P? x)
+map : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
+      P ≐ Q → Decidable P → Decidable Q
+map (P⊆Q , Q⊆P) P? x = map′ P⊆Q Q⊆P (P? x)
 
 ∁? : {P : Pred A ℓ} → Decidable P → Decidable (∁ P)
 ∁? P? x = ¬? (P? x)
@@ -244,7 +244,7 @@ does-≡ P? P?′ x = Dec.does-≡ (P? x) (P?′ x)
 does-≐ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} → P ≐ Q →
          (P? : Decidable P) → (Q? : Decidable Q) →
          does ∘ P? ≗ does ∘ Q?
-does-≐ P≐Q P? = does-≡ (≐? P≐Q P?)
+does-≐ P≐Q P? = does-≡ (map P≐Q P?)
 
 ------------------------------------------------------------------------
 -- Irrelevant properties