[ new ] symmetric core of a binary relation (#2071)

* [ new ] symmetric core of a binary relation

* [ fix ] name clashes

* [ more ] respond to McKinna's comments

* [ rename ] fields to lhs≤rhs and rhs≤lhs

* [ more ] incorporate parts of McKinna's review

* [ minor ] remove implicit argument application from transitive

* [ edit ] pull out isEquivalence and do some renaming

* [ minor ] respond to easy comments

* [ refactor ] remove IsProset, and move Proset to main hierarchy

* Eliminate Proset

* Fixed CHANGELOG typo

---------

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

CHANGELOG.md

@@ -49,6 +49,11 @@ Deprecated names
 New modules
 -----------
 
+* Symmetric interior of a binary relation
+ ```
+ Relation.Binary.Construct.Interior.Symmetric
+ ```
+
 * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures
 
 * Nagata's construction of the "idealization of a module":
@@ -205,9 +210,10 @@ Additions to existing modules
 * In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can
  be used infix.
 
-* Added new definitions in `Relation.Binary`
+* Added new definitions in `Relation.Binary.Definitions`
  ```
- Stable : Pred A ℓ → Set _
+ Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y)
+ Empty _∼_ = ∀ {x y} → x ∼ y → ⊥
  ```
 
 * Added new proofs in `Relation.Binary.Properties.Setoid`:

src/Data/Fin/Subset/Properties.agda

@@ -35,7 +35,7 @@ open import Relation.Binary.Structures
  using (IsPreorder; IsPartialOrder; IsStrictPartialOrder; IsDecStrictPartialOrder)
 open import Relation.Binary.Bundles
  using (Preorder; Poset; StrictPartialOrder; DecStrictPartialOrder)
-open import Relation.Binary.Definitions as B hiding (Decidable)
+open import Relation.Binary.Definitions as B hiding (Decidable; Empty)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_)
 open import Relation.Nullary.Negation using (contradiction)

src/Relation/Binary/Construct/Interior/Symmetric.agda

@@ -0,0 +1,83 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Symmetric interior of a binary relation
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Construct.Interior.Symmetric where
+
+open import Function.Base using (flip)
+open import Level
+open import Relation.Binary
+
+private
+ variable
+ a b c ℓ r s t : Level
+ A : Set a
+ R S T : Rel A r
+
+------------------------------------------------------------------------
+-- Definition
+
+record SymInterior (R : Rel A ℓ) (x y : A) : Set ℓ where
+ constructor _,_
+ field
+ lhs≤rhs : R x y
+ rhs≤lhs : R y x
+
+open SymInterior public
+
+------------------------------------------------------------------------
+-- Properties
+
+-- The symmetric interior is symmetric.
+symmetric : Symmetric (SymInterior R)
+symmetric (r , r′) = r′ , r
+
+-- The symmetric interior of R is greater than (or equal to) any other symmetric
+-- relation contained by R.
+unfold : Symmetric S → S ⇒ R → S ⇒ SymInterior R
+unfold sym f s = f s , f (sym s)
+
+-- SymInterior preserves various properties.
+reflexive : Reflexive R → Reflexive (SymInterior R)
+reflexive refl = refl , refl
+
+trans : Trans R S T → Trans S R T →
+ Trans (SymInterior R) (SymInterior S) (SymInterior T)
+trans trans-rs trans-sr (r , r′) (s , s′) = trans-rs r s , trans-sr s′ r′
+
+transitive : Transitive R → Transitive (SymInterior R)
+transitive tr = trans tr tr
+
+-- The symmetric interior of a strict relation is empty.
+asymmetric⇒empty : Asymmetric R → Empty (SymInterior R)
+asymmetric⇒empty asym (r , r′) = asym r r′
+
+-- A reflexive transitive relation _≤_ gives rise to a poset in which the
+-- equivalence relation is SymInterior _≤_.
+
+isEquivalence : Reflexive R → Transitive R → IsEquivalence (SymInterior R)
+isEquivalence refl trans = record
+ { refl = reflexive refl
+ ; sym = symmetric
+ ; trans = transitive trans
+ }
+
+isPartialOrder : Reflexive R → Transitive R → IsPartialOrder (SymInterior R) R
+isPartialOrder refl trans = record
+ { isPreorder = record
+ { isEquivalence = isEquivalence refl trans
+ ; reflexive = lhs≤rhs
+ ; trans = trans
+ }
+ ; antisym = _,_
+ }
+
+poset : ∀ {a} {A : Set a} {R : Rel A ℓ} → Reflexive R → Transitive R → Poset a ℓ ℓ
+poset {R = R} refl trans = record
+ { _≤_ = R
+ ; isPartialOrder = isPartialOrder refl trans
+ }

src/Relation/Binary/Definitions.agda

@@ -12,6 +12,8 @@ module Relation.Binary.Definitions where
 
 open import Agda.Builtin.Equality using (_≡_)
 
+open import Data.Empty using (⊥)
+open import Data.Maybe.Base using (Maybe)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_on_; flip)
@@ -243,6 +245,11 @@ DecidableEquality A = Decidable {A = A} _≡_
 Universal : REL A B ℓ → Set _
 Universal _∼_ = ∀ x y → x ∼ y
 
+-- Empty - no elements are related
+
+Empty : REL A B ℓ → Set _
+Empty _∼_ = ∀ {x y} → x ∼ y → ⊥
+
 -- Non-emptiness - at least one pair of elements are related.
 
 record NonEmpty {A : Set a} {B : Set b}

src/Relation/Unary/Polymorphic/Properties.agda

@@ -10,7 +10,7 @@
 module Relation.Unary.Polymorphic.Properties where
 
 open import Level using (Level)
-open import Relation.Binary.Definitions hiding (Decidable; Universal)
+open import Relation.Binary.Definitions hiding (Decidable; Universal; Empty)
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Unary hiding (∅; U)
 open import Relation.Unary.Polymorphic

src/Relation/Unary/Properties.agda

@@ -13,7 +13,8 @@ open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Unit.Base using (tt)
 open import Level using (Level)
 open import Relation.Binary.Core as Binary
-open import Relation.Binary.Definitions hiding (Decidable; Universal; Irrelevant)
+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_; ¬?)