From 78bd91bd983324c2c6dab309d7a533e96b4d185a Mon Sep 17 00:00:00 2001
From: Bradley Saul <bradleysaul@fastmail.com>
Date: Wed, 19 Feb 2025 11:28:08 -0500
Subject: [PATCH 1/7] add disjoint relation

---
 src/Relation/Unary.agda | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 3abc070ace..3a9aaddd3b 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -207,7 +207,7 @@ infixr 8 _⇒_
 infixr 7 _∩_
 infixr 6 _∪_
 infixr 6 _∖_
-infix 4 _≬_
+infix 4 _≬_ _#_ _#′_
 
 -- Complement.
 
@@ -253,6 +253,14 @@ syntax ⋂ I (λ i → P) = ⋂[ i ∶ I ] P
 _≬_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
 P ≬ Q = ∃ λ x → x ∈ P × x ∈ Q
 
+-- Disjoint
+
+_#_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P # Q = P ∩ Q ⊆ ∅
+
+_#′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P #′ Q = P ∩ Q ⊆′ ∅
+
 -- Update.
 
 _⊢_ : (A → B) → Pred B ℓ → Pred A ℓ

From 1a8225e37f3fb6ea143a06bf3b2dd590252f743f Mon Sep 17 00:00:00 2001
From: Bradley Saul <bradleysaul@fastmail.com>
Date: Wed, 19 Feb 2025 11:28:15 -0500
Subject: [PATCH 2/7] update changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 468a6e6915..71320bfd24 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -143,3 +143,8 @@ Additions to existing modules
   ```agda
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
+
+* In `Relation.Unary`:
+  ```agda
+  _#_ _#′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+  ```

From c48d4b8799092307ed00778e66af32edfe40626a Mon Sep 17 00:00:00 2001
From: Bradley Saul <bradleysaul@fastmail.com>
Date: Wed, 19 Feb 2025 14:15:45 -0500
Subject: [PATCH 3/7] try out perp instead of #

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 71320bfd24..0977e9a178 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -146,5 +146,5 @@ Additions to existing modules
 
 * In `Relation.Unary`:
   ```agda
-  _#_ _#′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+  _⊥_ _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
   ```
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 3a9aaddd3b..1d70e5bc8e 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -255,11 +255,11 @@ P ≬ Q = ∃ λ x → x ∈ P × x ∈ Q
 
 -- Disjoint
 
-_#_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
-P # Q = P ∩ Q ⊆ ∅
+_⊥_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊥ Q = P ∩ Q ⊆ ∅
 
-_#′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
-P #′ Q = P ∩ Q ⊆′ ∅
+_⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊥′ Q = P ∩ Q ⊆′ ∅
 
 -- Update.
 

From 8ff21724d419cd337489a11000eaf793ba5cb556 Mon Sep 17 00:00:00 2001
From: Bradley Saul <bradleysaul@fastmail.com>
Date: Wed, 19 Feb 2025 14:19:01 -0500
Subject: [PATCH 4/7] fix infix

---
 src/Relation/Unary.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 1d70e5bc8e..86bb80f1bb 100644
--- a/src/Relation/Unary.agda
+++ b/src/Relation/Unary.agda
@@ -207,7 +207,7 @@ infixr 8 _⇒_
 infixr 7 _∩_
 infixr 6 _∪_
 infixr 6 _∖_
-infix 4 _≬_ _#_ _#′_
+infix 4 _≬_ _⊥_ _⊥′_
 
 -- Complement.
 

From f77d38bcc8b6ae036cc389e30aa4029bde3c5ad6 Mon Sep 17 00:00:00 2001
From: Bradley Saul <bradleysaul@fastmail.com>
Date: Fri, 21 Feb 2025 14:58:41 -0500
Subject: [PATCH 5/7] Adds a few properties of disjoint relation

---
 CHANGELOG.md                       |  8 ++++++++
 src/Relation/Unary/Properties.agda | 18 +++++++++++++++++-
 2 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0977e9a178..e0caa538cd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -148,3 +148,11 @@ Additions to existing modules
   ```agda
   _⊥_ _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
   ```
+
+* In `Relation.Unary.Definitions`:
+  ```agda
+  ≬-sym : Symmetric {A = Pred A ℓ₁} _≬_
+  ⊥-sym : Symmetric {A = Pred A ℓ₁} _⊥_
+  ≬⇒¬⊥ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≬_ (¬_ ∘₂ _⊥_)
+  ⊥⇒¬≬ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊥_ (¬_ ∘₂ _≬_)
+  ```
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index 5a108d9081..b10c45f844 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -18,7 +18,8 @@ open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality.Core using (refl; _≗_)
 open import Relation.Unary
 open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
-open import Function.Base using (id; _$_; _∘_)
+open import Relation.Nullary.Negation using (¬_)
+open import Function.Base using (id; _$_; _∘_; _∘₂_)
 
 private
   variable
@@ -197,6 +198,21 @@ U-Universal = λ _ → _
 ≐′⇒≐ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐′_ _≐_
 ≐′⇒≐ = Product.map ⊆′⇒⊆ ⊆′⇒⊆
 
+------------------------------------------------------------------------
+-- Between/Disjoint properties
+
+≬-sym : Symmetric {A = Pred A ℓ₁} _≬_
+≬-sym = Product.map₂ swap
+
+⊥-sym : Symmetric {A = Pred A ℓ₁} _⊥_
+⊥-sym = _∘ swap
+
+≬⇒¬⊥ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≬_ (¬_ ∘₂ _⊥_)
+≬⇒¬⊥ P≬Q ¬P⊥Q = ¬P⊥Q (Product.proj₂ P≬Q)
+
+⊥⇒¬≬ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊥_ (¬_ ∘₂ _≬_)
+⊥⇒¬≬ P⊥Q = P⊥Q ∘ Product.proj₂
+
 ------------------------------------------------------------------------
 -- Decidability properties
 

From 07229e513c5a9be4b27587e2cea53cd8740abdbc Mon Sep 17 00:00:00 2001
From: Bradley Saul <bradleysaul@fastmail.com>
Date: Mon, 24 Feb 2025 14:44:18 -0500
Subject: [PATCH 6/7] specialize Negation import to Core

---
 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 b10c45f844..3bc0219d8e 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
 open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_)
 open import Function.Base using (id; _$_; _∘_; _∘₂_)
 
 private

From 289155735a434d2e6b8cd6f427dc450de539bfbb Mon Sep 17 00:00:00 2001
From: Bradley Saul <bradleysaul@fastmail.com>
Date: Wed, 26 Feb 2025 11:47:05 -0500
Subject: [PATCH 7/7] Update CHANGELOG.md

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e0caa538cd..2b1c46f309 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -149,7 +149,7 @@ Additions to existing modules
   _⊥_ _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
   ```
 
-* In `Relation.Unary.Definitions`:
+* In `Relation.Unary.Properties`:
   ```agda
   ≬-sym : Symmetric {A = Pred A ℓ₁} _≬_
   ⊥-sym : Symmetric {A = Pred A ℓ₁} _⊥_