Adds unary disjoint relation (#2595)

* add disjoint relation

* update changelog

* try out perp instead of #

* fix infix

* Adds a few properties of disjoint relation

* specialize Negation import to Core

* Update CHANGELOG.md

Co-authored-by: jamesmckinna <[email protected]>

* Update src/Relation/Unary/Properties.agda

Refactor to achieve greater level polymorphism

* Update CHANGELOG.md

Simplify types

---------

Co-authored-by: jamesmckinna <[email protected]>
Co-authored-by: Matthew Daggitt <[email protected]>

Author: 3 people

CHANGELOG.md

@@ -377,6 +377,20 @@ Additions to existing modules
   ⊥-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 _⊥_
+  ≬⇒¬⊥ : _≬_ ⇒  (¬_ ∘₂ _⊥_)
+  ⊥⇒¬≬ : _⊥_ ⇒  (¬_ ∘₂ _≬_)
+
 * In `Relation.Nullary.Negation.Core`:
   ```agda
   contra-diagonal : (A → ¬ A) → ¬ A

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 ℓ

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