Ob #453: added Dense relations and DenseLinearOrder

CHANGELOG.md

@@ -3019,6 +3019,7 @@ Additions to existing modules
 
 * Added new definitions in `Relation.Binary.Definitions`:
   ```
+  Dense        _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y
   Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y)
   Tight    _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y)
 
@@ -3033,11 +3034,13 @@ Additions to existing modules
 
 * Added new definitions in `Relation.Binary.Bundles`:
   ```
+  record DenseLinearOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   ```
 
 * Added new definitions in `Relation.Binary.Structures`:
   ```
+  record IsDenseLinearOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   ```
 

src/Data/Tree/AVL/Indexed/WithK.agda

@@ -15,6 +15,7 @@ module Data.Tree.AVL.Indexed.WithK
        {k r} (Key : Set k) {_<_ : Rel Key r}
        (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where
 
+strictTotalOrder : StrictTotalOrder _ _ _
 strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder }
 
 open import Data.Tree.AVL.Indexed strictTotalOrder as AVL hiding (Value)

src/Data/Tree/AVL/NonEmpty/Propositional.agda

@@ -17,7 +17,9 @@ module Data.Tree.AVL.NonEmpty.Propositional
 
 open import Level
 
-private strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder}
+private
+  strictTotalOrder : StrictTotalOrder _ _ _
+  strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder}
 open import Data.Tree.AVL.Value (StrictTotalOrder.Eq.setoid strictTotalOrder)
 import Data.Tree.AVL.NonEmpty strictTotalOrder as AVL⁺
 

src/Relation/Binary/Bundles.agda

@@ -299,6 +299,23 @@ record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wh
   Please use Eq.decSetoid instead."
   #-}
 
+record DenseLinearOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _<_
+  field
+    Carrier            : Set c
+    _≈_                : Rel Carrier ℓ₁
+    _<_                : Rel Carrier ℓ₂
+    isDenseLinearOrder : IsDenseLinearOrder _≈_ _<_
+
+  open IsDenseLinearOrder isDenseLinearOrder public
+
+  strictTotalOrder : StrictTotalOrder c ℓ₁ ℓ₂
+  strictTotalOrder = record
+    { isStrictTotalOrder = isStrictTotalOrder
+    }
+
+  --open StrictTotalOrder strictTotalOrder public
+
 
 ------------------------------------------------------------------------
 -- Apartness relations

src/Relation/Binary/Definitions.agda

@@ -13,7 +13,7 @@ module Relation.Binary.Definitions where
 open import Agda.Builtin.Equality using (_≡_)
 
 open import Data.Maybe.Base using (Maybe)
-open import Data.Product.Base using (_×_)
+open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
 open import Function.Base using (_on_; flip)
 open import Level
@@ -88,6 +88,11 @@ Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y)
 Asymmetric : Rel A ℓ → Set _
 Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
 
+-- Density
+
+Dense : Rel A ℓ → Set _
+Dense _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y
+
 -- Generalised connex - exactly one of the two relations holds.
 
 Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _

src/Relation/Binary/Structures.agda

@@ -280,6 +280,14 @@ record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) wher
     using (irrefl; asym; <-respʳ-≈; <-respˡ-≈; <-resp-≈)
 
 
+record IsDenseLinearOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isStrictTotalOrder : IsStrictTotalOrder _<_
+    dense              : Dense _<_
+
+  open IsStrictTotalOrder isStrictTotalOrder public
+
+
 ------------------------------------------------------------------------
 -- Apartness relations
 ------------------------------------------------------------------------