diff --git a/CHANGELOG.md b/CHANGELOG.md
index a6f66aa2f5..efad7b2d60 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -244,3 +244,18 @@ Additions to existing modules
   ⊤-dec : Dec {a} ⊤
   ⊥-dec : Dec {a} ⊥
   ```
+
+* In `Relation.Unary`:
+  ```agda
+  _⊥_ _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+  ```
+
+* In `Relation.Unary.Properties`:
+  ```agda
+  ≬-symmetric : Sym _≬_ _≬_
+  ⊥-symmetric : Sym _⊥_ _⊥_
+  ≬-sym : Symmetric _≬_
+  ⊥-sym : Symmetric _⊥_
+  ≬⇒¬⊥ : _≬_ ⇒  (¬_ ∘₂ _⊥_)
+  ⊥⇒¬≬ : _⊥_ ⇒  (¬_ ∘₂ _≬_)
+  ```
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 3abc070ace..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.
 
@@ -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 ℓ
diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda
index 0cb06248a9..b16b6702b8 100644
--- a/src/Relation/Unary/Properties.agda
+++ b/src/Relation/Unary/Properties.agda
@@ -11,15 +11,16 @@ module Relation.Unary.Properties where
 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)
+open import Function.Base using (id; _$_; _∘_; _∘₂_)
 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.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.Core using (¬_)
+open import Relation.Unary
 
 private
   variable
@@ -198,6 +199,27 @@ U-Universal = λ _ → _
 ≐′⇒≐ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐′_ _≐_
 ≐′⇒≐ = Product.map ⊆′⇒⊆ ⊆′⇒⊆
 
+------------------------------------------------------------------------
+-- Between/Disjoint properties
+
+≬-symmetric : Sym {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≬_ _≬_
+≬-symmetric = Product.map₂ swap
+
+⊥-symmetric : Sym {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊥_ _⊥_
+⊥-symmetric = _∘ swap
+
+≬-sym : Symmetric {A = Pred A ℓ₁} _≬_
+≬-sym = ≬-symmetric
+
+⊥-sym : Symmetric {A = Pred A ℓ₁} _⊥_
+⊥-sym = ⊥-symmetric
+
+≬⇒¬⊥ : 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